Documentation

Foundation.FirstOrder.Arith.Model

@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_zero_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(0).term = op(0).term
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_one_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(1).term = op(1).term
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_add_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(+).term = op(+).term
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_mul_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(*).term = op(*).term
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_eq_val {L : LO.FirstOrder.Language} [L.ORing] :
(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) op(=).sentence = op(=).sentence
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_lt_val {L : LO.FirstOrder.Language} [L.ORing] :
(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) op(<).sentence = op(<).sentence
Equations
  • One or more equations did not get rendered due to their size.
structure LO.FirstOrder.Arith.Cut (L : LO.FirstOrder.Language) [L.ORing] (M : Type w) [s : LO.FirstOrder.Structure L M] :
Instances For
    Instances For