Documentation

Foundation.FirstOrder.Basic.Operator

source
structure LO.FirstOrder.Semiterm.Operator (L : Language) (n : ℕ) :
Type u_1
source
@[reducible, inline]
abbrev LO.FirstOrder.Semiterm.Const (L : Language) :
Type u
Equations
Instances For
source
def LO.FirstOrder.Semiterm.fn {L : Language} {k : ℕ} (f : L.Func k) :
Operator L k
Equations
source
def LO.FirstOrder.Semiterm.Operator.equiv {L : Language} {n : ℕ} :
Operator L n ≃ Semiterm L Empty n
Equations
source
def LO.FirstOrder.Semiterm.Operator.operator {L : Language} {ξ : Type u_2} {n arity : ℕ} (o : Operator L arity) (v : Fin arity → Semiterm L ξ n) :
Semiterm L ξ n
Equations
source
@[reducible, inline]
abbrev LO.FirstOrder.Semiterm.Operator.const {L : Language} {ξ : Type u_2} {n : ℕ} (c : Const L) :
Semiterm L ξ n
Equations
source
instance LO.FirstOrder.Semiterm.Operator.instCoeConst {L : Language} {ξ : Type u_2} {n : ℕ} :
Coe (Const L) (Semiterm L ξ n)
Equations
source
def LO.FirstOrder.Semiterm.Operator.comp {L : Language} {k l : ℕ} (o : Operator L k) (w : Fin k → Operator L l) :
Operator L l
Equations
  • o.comp w = { term := o.operator fun (x : Fin k) => (w x).term }
source
@[simp]
theorem LO.FirstOrder.Semiterm.Operator.operator_comp {L : Language} {k l : ℕ} {ξ : Type u_1} {n : ℕ} (o : Operator L k) (w : Fin k → Operator L l) (v : Fin l → Semiterm L ξ n) :
(o.comp w).operator v = o.operator fun (x : Fin k) => (w x).operator v
source
def LO.FirstOrder.Semiterm.Operator.bvar {L : Language} {n : ℕ} (x : Fin n) :
Operator L n
Equations
source
theorem LO.FirstOrder.Semiterm.Operator.operator_bvar {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (x : Fin k) (v : Fin k → Semiterm L ξ n) :
(bvar x).operator v = v x
source
theorem LO.FirstOrder.Semiterm.Operator.bv_operator {L : Language} {ξ : Type u_1} {n k : ℕ} (o : Operator L k) (v : Fin k → Semiterm L ξ (n + 1)) :
(o.operator v).bv = o.term.bv.biUnion fun (i : Fin k) => (v i).bv
source
theorem LO.FirstOrder.Semiterm.Operator.positive_operator_iff {L : Language} {ξ : Type u_1} {n k : ℕ} {o : Operator L k} {v : Fin k → Semiterm L ξ (n + 1)} :
(o.operator v).Positive ↔ ∀ i ∈ o.term.bv, (v i).Positive
source
@[simp]
theorem LO.FirstOrder.Semiterm.Operator.positive_const {L : Language} {ξ : Type u_1} {n : ℕ} (c : Const L) :
(↑c).Positive
source
def LO.FirstOrder.Semiterm.Operator.foldr {L : Language} {k : ℕ} (f : Operator L 2) (z : Operator L k) :
List (Operator L k) → Operator L k
Equations
  • f.foldr z [] = z
  • f.foldr z (o :: os) = f.comp ![f.foldr z os, o]
source
@[simp]
theorem LO.FirstOrder.Semiterm.Operator.foldr_nil {L : Language} {k : ℕ} (f : Operator L 2) (z : Operator L k) :
f.foldr z [] = z
source
@[simp]
theorem LO.FirstOrder.Semiterm.Operator.operator_foldr_cons {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (f : Operator L 2) (z o : Operator L k) (os : List (Operator L k)) (v : Fin k → Semiterm L ξ n) :
(f.foldr z (o :: os)).operator v = f.operator ![(f.foldr z os).operator v, o.operator v]
source
def LO.FirstOrder.Semiterm.Operator.iterr {L : Language} (f : Operator L 2) (z : Const L) (n : ℕ) :
Operator L n
Equations
source
@[simp]
theorem LO.FirstOrder.Semiterm.Operator.iterr_zero {L : Language} (f : Operator L 2) (z : Const L) :
f.iterr z 0 = z
source
class LO.FirstOrder.Semiterm.Operator.Zero (L : Language) :
Type u_1
Instances
source
class LO.FirstOrder.Semiterm.Operator.One (L : Language) :
Type u_1
Instances
source
class LO.FirstOrder.Semiterm.Operator.Add (L : Language) :
Type u_1
Instances
source
class LO.FirstOrder.Semiterm.Operator.Mul (L : Language) :
Type u_1
Instances
source
class LO.FirstOrder.Semiterm.Operator.Exp (L : Language) :
Type u_1
Instances
source
class LO.FirstOrder.Semiterm.Operator.Sub (L : Language) :
Type u_1
Instances
    source
    class LO.FirstOrder.Semiterm.Operator.Div (L : Language) :
    Type u_1
    Instances
      source
      class LO.FirstOrder.Semiterm.Operator.Star (L : Language) :
      Type u_1
      Instances
      source
      class LO.FirstOrder.Semiterm.Operator.GoedelNumber (L : Language) (α : Type u_1) :
      Type (max u_1 u_2)
      • goedelNumber : α → Const L
      Instances
      source
      def LO.FirstOrder.Semiterm.Operator.«termOp(0)» :
      Lean.ParserDescr
      Equations
      source
      def LO.FirstOrder.Semiterm.Operator.«termOp(1)» :
      Lean.ParserDescr
      Equations
      source
      def LO.FirstOrder.Semiterm.Operator.«termOp(+)» :
      Lean.ParserDescr
      Equations
      source
      def LO.FirstOrder.Semiterm.Operator.«termOp(*)» :
      Lean.ParserDescr
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.instZeroOfZero {L : Language} [L.Zero] :
      Operator.Zero L
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.instOneOfOne {L : Language} [L.One] :
      Operator.One L
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.instAddOfAdd {L : Language} [L.Add] :
      Operator.Add L
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.instMulOfMul {L : Language} [L.Mul] :
      Operator.Mul L
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.instExpOfExp {L : Language} [L.Exp] :
      Operator.Exp L
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.instStarOfStar {L : Language} [L.Star] :
      Operator.Star L
      Equations
      source
      theorem LO.FirstOrder.Semiterm.Operator.Zero.term_eq {L : Language} [L.Zero] :
      op(0).term = func Language.Zero.zero ![]
      source
      theorem LO.FirstOrder.Semiterm.Operator.One.term_eq {L : Language} [L.One] :
      op(1).term = func Language.One.one ![]
      source
      theorem LO.FirstOrder.Semiterm.Operator.Add.term_eq {L : Language} [L.Add] :
      op(+).term = func Language.Add.add Semiterm.bvar
      source
      theorem LO.FirstOrder.Semiterm.Operator.Mul.term_eq {L : Language} [L.Mul] :
      op(*).term = func Language.Mul.mul Semiterm.bvar
      source
      theorem LO.FirstOrder.Semiterm.Operator.Exp.term_eq {L : Language} [L.Exp] :
      exp.term = func Language.Exp.exp Semiterm.bvar
      source
      theorem LO.FirstOrder.Semiterm.Operator.Star.term_eq {L : Language} [L.Star] :
      star.term = func Language.Star.star ![]
      source
      def LO.FirstOrder.Semiterm.Operator.numeral (L : Language) [Operator.Zero L] [Operator.One L] [Operator.Add L] :
      ℕ → Const L
      Equations
      source
      theorem LO.FirstOrder.Semiterm.Operator.numeral_zero {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] :
      numeral L 0 = op(0)
      source
      theorem LO.FirstOrder.Semiterm.Operator.numeral_one {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] :
      numeral L 1 = op(1)
      source
      theorem LO.FirstOrder.Semiterm.Operator.numeral_succ {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] {z : ℕ} :
      z ≠ 0 → numeral L (z + 1) = op(+).comp ![numeral L z, op(1)]
      source
      theorem LO.FirstOrder.Semiterm.Operator.numeral_add_two {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] {z : ℕ} :
      numeral L (z + 2) = op(+).comp ![numeral L (z + 1), op(1)]
      source
      @[reducible, inline]
      abbrev LO.FirstOrder.Semiterm.Operator.encode (L : Language) [Operator.Zero L] [Operator.One L] [Operator.Add L] {α : Type u_1} [Encodable α] (a : α) :
      Const L
      Equations
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.Operator.Add.positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [L.Add] (t u : Semiterm L ξ (n + 1)) :
      (op(+).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.Operator.Mul.positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [L.Mul] (t u : Semiterm L ξ (n + 1)) :
      (op(*).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.Operator.Exp.positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [L.Exp] (t : Semiterm L ξ (n + 1)) :
      (exp.operator ![t]).Positive ↔ t.Positive
      source
      def LO.FirstOrder.Semiterm.Operator.npow (L : Language) [Operator.One L] [Operator.Mul L] (n : ℕ) :
      Operator L 1
      Equations
      source
      theorem LO.FirstOrder.Semiterm.Operator.npow_zero {L : Language} [Operator.One L] [Operator.Mul L] :
      npow L 0 = comp op(1) ![]
      source
      theorem LO.FirstOrder.Semiterm.Operator.npow_succ {L : Language} [Operator.One L] [Operator.Mul L] {n : ℕ} :
      npow L (n + 1) = op(*).comp ![npow L n, bvar 0]
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.Operator.npow_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [Operator.One L] [L.Mul] (t : Semiterm L ξ (n + 1)) (k : ℕ) :
      ((npow L k).operator ![t]).Positive ↔ k = 0 ∨ t.Positive
      source
      @[reducible, inline]
      abbrev LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber' {L : Language} {α : Type u_2} [GoedelNumber L α] {ξ : Type u_3} {n : ℕ} (a : α) :
      Semiterm L ξ n
      Equations
      source
      instance LO.FirstOrder.Semiterm.Operator.GoedelNumber.instGoedelQuote {L : Language} {α : Type u_2} [GoedelNumber L α] {ξ : Type u_3} {n : ℕ} :
      GoedelQuote α (Semiterm L ξ n)
      Equations
      source
      def LO.FirstOrder.Semiterm.Operator.GoedelNumber.ofEncodable {L : Language} [Operator.Zero L] [Operator.One L] [Operator.Add L] {α : Type u_1} [Encodable α] :
      GoedelNumber L α
      Equations
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.complexity_zero {L : Language} {ξ : Type u_1} {n : ℕ} [L.Zero] :
      (↑op(0)).complexity = 1
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.complexity_one {L : Language} {ξ : Type u_1} {n : ℕ} [L.One] :
      (↑op(1)).complexity = 1
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.complexity_add {L : Language} {ξ : Type u_1} {n : ℕ} [L.Add] (t u : Semiterm L ξ n) :
      (op(+).operator ![t, u]).complexity = t.complexity ⊔ u.complexity + 1
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.complexity_mul {L : Language} {ξ : Type u_1} {n : ℕ} [L.Mul] (t u : Semiterm L ξ n) :
      (op(*).operator ![t, u]).complexity = t.complexity ⊔ u.complexity + 1
      source
      def LO.FirstOrder.Semiterm.Operator.val {L : Language} {k : ℕ} {M : Type w} [s : Structure L M] (o : Operator L k) (v : Fin k → M) :
      M
      Equations
      source
      theorem LO.FirstOrder.Semiterm.val_operator {L : Language} {M : Type w} {s : Structure L M} {n✝ : ℕ} {e : Fin n✝ → M} {ξ✝ : Type u_1} {ε : ξ✝ → M} {k : ℕ} (o : Operator L k) (v : Fin k → Semiterm L ξ✝ n✝) :
      val s e ε (o.operator v) = o.val fun (x : Fin k) => val s e ε (v x)
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.val_const {L : Language} {M : Type w} {s : Structure L M} {n✝ : ℕ} {e : Fin n✝ → M} {ξ✝ : Type u_1} {ε : ξ✝ → M} (o : Const L) :
      val s e ε ↑o = Operator.val o ![]
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.val_operator₀ {L : Language} {M : Type w} {s : Structure L M} {n✝ : ℕ} {e : Fin n✝ → M} {ξ✝ : Type u_1} {ε : ξ✝ → M} {v : Fin 0 → Semiterm L ξ✝ n✝} (o : Const L) :
      val s e ε (Operator.operator o v) = Operator.val o ![]
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.val_operator₁ {L : Language} {M : Type w} {s : Structure L M} {n✝ : ℕ} {e : Fin n✝ → M} {ξ✝ : Type u_1} {ε : ξ✝ → M} {t : Semiterm L ξ✝ n✝} (o : Operator L 1) :
      val s e ε (o.operator ![t]) = o.val ![val s e ε t]
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.val_operator₂ {L : Language} {M : Type w} {s : Structure L M} {n✝ : ℕ} {e : Fin n✝ → M} {ξ✝ : Type u_1} {ε : ξ✝ → M} (o : Operator L 2) (t u : Semiterm L ξ✝ n✝) :
      val s e ε (o.operator ![t, u]) = o.val ![val s e ε t, val s e ε u]
      source
      theorem LO.FirstOrder.Semiterm.Operator.val_comp {L : Language} {M : Type w} {s : Structure L M} {k m : ℕ} (o₁ : Operator L k) (o₂ : Fin k → Operator L m) (v : Fin m → M) :
      (o₁.comp o₂).val v = o₁.val fun (i : Fin k) => (o₂ i).val v
      source
      @[simp]
      theorem LO.FirstOrder.Semiterm.Operator.val_bvar {L : Language} {M : Type w} {s : Structure L M} {n : ℕ} (x : Fin n) (v : Fin n → M) :
      (bvar x).val v = v x
      source
      structure LO.FirstOrder.Semiformula.Operator (L : Language) (n : ℕ) :
      Type u
      source
      @[reducible, inline]
      abbrev LO.FirstOrder.Semiformula.Const (L : Language) :
      Type u
      Equations
      Instances For
      source
      def LO.FirstOrder.Semiformula.Operator.operator {L : Language} {ξ : Type u_2} {n arity : ℕ} (o : Operator L arity) (v : Fin arity → Semiterm L ξ n) :
      Semiformula L ξ n
      Equations
      • o.operator v = ↑o.sentence ⇜ v
      source
      def LO.FirstOrder.Semiformula.Operator.const {L : Language} {ξ : Type u_2} {n : ℕ} (c : Const L) :
      Semiformula L ξ n
      Equations
      source
      instance LO.FirstOrder.Semiformula.Operator.instCoeConst {L : Language} {ξ : Type u_2} {n : ℕ} :
      Coe (Const L) (Semiformula L ξ n)
      Equations
      source
      def LO.FirstOrder.Semiformula.Operator.comp {L : Language} {k l : ℕ} (o : Operator L k) (w : Fin k → Semiterm.Operator L l) :
      Operator L l
      Equations
      • o.comp w = { sentence := o.operator fun (x : Fin k) => (w x).term }
      source
      theorem LO.FirstOrder.Semiformula.Operator.operator_comp {L : Language} {k l : ℕ} {ξ : Type u_1} {n : ℕ} (o : Operator L k) (w : Fin k → Semiterm.Operator L l) (v : Fin l → Semiterm L ξ n) :
      (o.comp w).operator v = o.operator fun (x : Fin k) => (w x).operator v
      source
      def LO.FirstOrder.Semiformula.Operator.and {L : Language} {k : ℕ} (o₁ o₂ : Operator L k) :
      Operator L k
      Equations
      • o₁.and o₂ = { sentence := o₁.sentence ⋏ o₂.sentence }
      source
      def LO.FirstOrder.Semiformula.Operator.or {L : Language} {k : ℕ} (o₁ o₂ : Operator L k) :
      Operator L k
      Equations
      • o₁.or o₂ = { sentence := o₁.sentence ⋎ o₂.sentence }
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.operator_and {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (o₁ o₂ : Operator L k) (v : Fin k → Semiterm L ξ n) :
      (o₁.and o₂).operator v = o₁.operator v ⋏ o₂.operator v
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.operator_or {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (o₁ o₂ : Operator L k) (v : Fin k → Semiterm L ξ n) :
      (o₁.or o₂).operator v = o₁.operator v ⋎ o₂.operator v
      source
      class LO.FirstOrder.Semiformula.Operator.Eq (L : Language) :
      Type u_1
      Instances
      source
      class LO.FirstOrder.Semiformula.Operator.LT (L : Language) :
      Type u_1
      Instances
      source
      class LO.FirstOrder.Semiformula.Operator.LE (L : Language) :
      Type u_1
      Instances
      source
      class LO.FirstOrder.Semiformula.Operator.Mem (L : Language) :
      Type u_1
      Instances
      source
      def LO.FirstOrder.Semiformula.Operator.«termOp(=)» :
      Lean.ParserDescr
      Equations
      source
      def LO.FirstOrder.Semiformula.Operator.«termOp(<)» :
      Lean.ParserDescr
      Equations
      source
      def LO.FirstOrder.Semiformula.Operator.«termOp(≤)» :
      Lean.ParserDescr
      Equations
      source
      def LO.FirstOrder.Semiformula.Operator.«termOp(∈)» :
      Lean.ParserDescr
      Equations
      source
      instance LO.FirstOrder.Semiformula.Operator.instEqOfEq {L : Language} [L.Eq] :
      Operator.Eq L
      Equations
      source
      instance LO.FirstOrder.Semiformula.Operator.instLTOfLT {L : Language} [L.LT] :
      Operator.LT L
      Equations
      source
      instance LO.FirstOrder.Semiformula.Operator.instLEOfEqOfLT {L : Language} [Operator.Eq L] [Operator.LT L] :
      Operator.LE L
      Equations
      source
      theorem LO.FirstOrder.Semiformula.Operator.Eq.sentence_eq {L : Language} [L.Eq] :
      op(=).sentence = rel Language.Eq.eq Semiterm.bvar
      source
      theorem LO.FirstOrder.Semiformula.Operator.LT.sentence_eq {L : Language} [L.LT] :
      op(<).sentence = rel Language.LT.lt Semiterm.bvar
      source
      theorem LO.FirstOrder.Semiformula.Operator.LE.sentence_eq {L : Language} [L.Eq] [L.LT] :
      op(≤).sentence = op(=).sentence ⋎ op(<).sentence
      source
      theorem LO.FirstOrder.Semiformula.Operator.LE.def_of_Eq_of_LT {L : Language} [Operator.Eq L] [Operator.LT L] :
      op(≤) = op(=).or op(<)
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.Eq.equal_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Eq] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} :
      op(=).operator ![t₁, u₁] = op(=).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.LT.lt_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.LT] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} :
      op(<).operator ![t₁, u₁] = op(<).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.LE.le_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Eq] [L.LT] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} :
      op(≤).operator ![t₁, u₁] = op(≤).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
      source
      theorem LO.FirstOrder.Semiformula.Operator.lt_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t u : Semiterm L ξ n) :
      op(<).operator ![t, u] = rel Language.LT.lt ![t, u]
      source
      theorem LO.FirstOrder.Semiformula.Operator.eq_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] (t u : Semiterm L ξ n) :
      op(=).operator ![t, u] = rel Language.Eq.eq ![t, u]
      source
      theorem LO.FirstOrder.Semiformula.Operator.le_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] [L.LT] (t u : Semiterm L ξ n) :
      op(≤).operator ![t, u] = rel Language.Eq.eq ![t, u] ⋎ rel Language.LT.lt ![t, u]
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.Eq.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] (t u : Semiterm L ξ n) :
      (op(=).operator ![t, u]).Open
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.LT.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t u : Semiterm L ξ n) :
      (op(<).operator ![t, u]).Open
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.Operator.LE.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] [L.LT] (t u : Semiterm L ξ n) :
      (op(≤).operator ![t, u]).Open
      source
      def LO.FirstOrder.Semiformula.Operator.val {L : Language} {M : Type w} [s : Structure L M] {k : ℕ} (o : Operator L k) (v : Fin k → M) :
      Prop
      Equations
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.val_operator_and {L : Language} {M : Type w} {s : Structure L M} {k : ℕ} {o₁ o₂ : Operator L k} {v : Fin k → M} :
      (o₁.and o₂).val v ↔ o₁.val v ∧ o₂.val v
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.val_operator_or {L : Language} {M : Type w} {s : Structure L M} {k : ℕ} {o₁ o₂ : Operator L k} {v : Fin k → M} :
      (o₁.or o₂).val v ↔ o₁.val v ∨ o₂.val v
      source
      theorem LO.FirstOrder.Semiformula.eval_operator {L : Language} {M : Type w} {s : Structure L M} {ξ : Type u_1} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {k : ℕ} {o : Operator L k} {v : Fin k → Semiterm L ξ n} :
      (Eval s e ε) (o.operator v) ↔ o.val fun (i : Fin k) => Semiterm.val s e ε (v i)
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_operator₀ {L : Language} {M : Type w} {s : Structure L M} {n✝ : ℕ} {e : Fin n✝ → M} {ξ✝ : Type u_1} {ε : ξ✝ → M} {o : Const L} {v : Fin 0 → Semiterm L ξ✝ n✝} :
      (Eval s e ε) (Operator.operator o v) ↔ Operator.val o ![]
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_operator₁ {L : Language} {M : Type w} {s : Structure L M} {ξ : Type u_1} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {o : Operator L 1} {t : Semiterm L ξ n} :
      (Eval s e ε) (o.operator ![t]) ↔ o.val ![Semiterm.val s e ε t]
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_operator₂ {L : Language} {M : Type w} {s : Structure L M} {ξ : Type u_1} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {o : Operator L 2} {t₁ t₂ : Semiterm L ξ n} :
      (Eval s e ε) (o.operator ![t₁, t₂]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
      source
      def LO.FirstOrder.Semiformula.ballLT {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LT L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) :
      Semiformula L ξ n
      Equations
      source
      def LO.FirstOrder.Semiformula.bexLT {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LT L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) :
      Semiformula L ξ n
      Equations
      source
      def LO.FirstOrder.Semiformula.ballLE {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LE L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) :
      Semiformula L ξ n
      Equations
      source
      def LO.FirstOrder.Semiformula.bexLE {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LE L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) :
      Semiformula L ξ n
      Equations
      source
      def LO.FirstOrder.Semiformula.ballMem {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.Mem L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) :
      Semiformula L ξ n
      Equations
      source
      def LO.FirstOrder.Semiformula.bexMem {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.Mem L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) :
      Semiformula L ξ n
      Equations
      source
      theorem LO.FirstOrder.Rew.operator {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiterm.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) :
      ω (o.operator v) = o.operator fun (i : Fin k) => ω (v i)
      source
      theorem LO.FirstOrder.Rew.operator' {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiterm.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) :
      ω (o.operator v) = o.operator (⇑ω ∘ v)
      source
      @[simp]
      theorem LO.FirstOrder.Rew.finitary0 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 0) (v : Fin 0 → Semiterm L ξ₁ n₁) :
      ω (o.operator v) = o.operator ![]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.finitary1 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 1) (t : Semiterm L ξ₁ n₁) :
      ω (o.operator ![t]) = o.operator ![ω t]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.finitary2 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 2) (t₁ t₂ : Semiterm L ξ₁ n₁) :
      ω (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.finitary3 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 3) (t₁ t₂ t₃ : Semiterm L ξ₁ n₁) :
      ω (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.const {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_1} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (c : Semiterm.Const L) :
      ω ↑c = ↑c
      source
      theorem LO.FirstOrder.Rew.hom_operator {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiformula.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) :
      (Rewriting.app ω) (o.operator v) = o.operator fun (i : Fin k) => ω (v i)
      source
      theorem LO.FirstOrder.Rew.hom_operator' {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiformula.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) :
      (Rewriting.app ω) (o.operator v) = o.operator (⇑ω ∘ v)
      source
      @[simp]
      theorem LO.FirstOrder.Rew.hom_finitary0 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 0) (v : Fin 0 → Semiterm L ξ₁ n₁) :
      (Rewriting.app ω) (o.operator v) = o.operator ![]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.hom_finitary1 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 1) (t : Semiterm L ξ₁ n₁) :
      (Rewriting.app ω) (o.operator ![t]) = o.operator ![ω t]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.hom_finitary2 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 2) (t₁ t₂ : Semiterm L ξ₁ n₁) :
      (Rewriting.app ω) (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.hom_finitary3 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 3) (t₁ t₂ t₃ : Semiterm L ξ₁ n₁) :
      (Rewriting.app ω) (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]
      source
      @[simp]
      theorem LO.FirstOrder.Rew.hom_const {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_1} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {c : Semiformula.Const L} :
      (Rewriting.app ω) ↑c = ↑c
      source
      theorem LO.FirstOrder.Rew.eq_equal_iff {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) [L.Eq] {φ : Semiformula L ξ₁ n₁} {t u : Semiterm L ξ₂ n₂} :
      (Rewriting.app ω) φ = op(=).operator ![t, u] ↔ ∃ (t' : Semiterm L ξ₁ n₁) (u' : Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ φ = op(=).operator ![t', u']
      source
      theorem LO.FirstOrder.Rew.eq_lt_iff {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) [L.LT] {φ : Semiformula L ξ₁ n₁} {t u : Semiterm L ξ₂ n₂} :
      (Rewriting.app ω) φ = op(<).operator ![t, u] ↔ ∃ (t' : Semiterm L ξ₁ n₁) (u' : Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ φ = op(<).operator ![t', u']
      source
      class LO.FirstOrder.Structure.Zero (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Zero L] [Zero M] :
      Prop
      Instances
      source
      class LO.FirstOrder.Structure.One (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.One L] [One M] :
      Prop
      Instances
      source
      class LO.FirstOrder.Structure.Add (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Add L] [Add M] :
      Prop
      • add (a b : M) : op(+).val ![a, b] = a + b
      Instances
      source
      class LO.FirstOrder.Structure.Mul (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Mul L] [Mul M] :
      Prop
      • mul (a b : M) : op(*).val ![a, b] = a * b
      Instances
      source
      class LO.FirstOrder.Structure.Exp (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Exp L] [Exp M] :
      Prop
      Instances
      source
      class LO.FirstOrder.Structure.Eq (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.Eq L] :
      Prop
      Instances
      source
      class LO.FirstOrder.Structure.LT (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.LT L] [LT M] :
      Prop
      Instances
      source
      class LO.FirstOrder.Structure.LE (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.LE L] [LE M] :
      Prop
      Instances
      source
      class LO.FirstOrder.Structure.Mem (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.Mem L] [Membership M M] :
      Prop
      Instances
      source
      instance LO.FirstOrder.Structure.instLEOfEqOfLT (L : Language) (M : Type u_1) [Structure L M] [L.Eq] [L.LT] [Structure.Eq L M] [PartialOrder M] [Structure.LT L M] :
      Structure.LE L M
      source
      @[simp]
      theorem LO.FirstOrder.Structure.zero_eq_of_lang {L : Language} (M : Type u_1) [Structure L M] [L.Zero] [Zero M] [Structure.Zero L M] :
      func Language.Zero.zero ![] = 0
      source
      @[simp]
      theorem LO.FirstOrder.Structure.one_eq_of_lang {L : Language} (M : Type u_1) [Structure L M] [L.One] [One M] [Structure.One L M] :
      func Language.One.one ![] = 1
      source
      @[simp]
      theorem LO.FirstOrder.Structure.add_eq_of_lang {L : Language} (M : Type u_1) [Structure L M] [L.Add] [Add M] [Structure.Add L M] {v : Fin 2 → M} :
      func Language.Add.add v = v 0 + v 1
      source
      @[simp]
      theorem LO.FirstOrder.Structure.mul_eq_of_lang {L : Language} (M : Type u_1) [Structure L M] [L.Mul] [Mul M] [Structure.Mul L M] {v : Fin 2 → M} :
      func Language.Mul.mul v = v 0 * v 1
      source
      @[simp]
      theorem LO.FirstOrder.Structure.exp_eq_of_lang {L : Language} (M : Type u_1) [Structure L M] [L.Exp] [Exp M] [Structure.Exp L M] {v : Fin 1 → M} :
      func Language.Exp.exp v = exp (v 0)
      source
      theorem LO.FirstOrder.Structure.le_iff_of_eq_of_lt {L : Language} (M : Type u_1) [Structure L M] [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] [LT M] [Structure.Eq L M] [Structure.LT L M] {a b : M} :
      op(≤).val ![a, b] ↔ a = b ∨ a < b
      source
      @[simp]
      theorem LO.FirstOrder.Structure.eq_lang {L : Language} (M : Type u_1) [Structure L M] [L.Eq] [Structure.Eq L M] {v : Fin 2 → M} :
      rel Language.Eq.eq v ↔ v 0 = v 1
      source
      @[simp]
      theorem LO.FirstOrder.Structure.lt_lang {L : Language} (M : Type u_1) [Structure L M] [L.LT] [LT M] [Structure.LT L M] {v : Fin 2 → M} :
      rel Language.LT.lt v ↔ v 0 < v 1
      source
      theorem LO.FirstOrder.Structure.operator_val_ofEquiv_iff {L : Language} (M : Type u_1) [Structure L M] {N : Type u_2} (φ : M ≃ N) {k : ℕ} {o : Semiformula.Operator L k} {v : Fin k → N} :
      o.val v ↔ o.val (⇑φ.symm ∘ v)
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_ballLT {ξ : Type u_3} {n : ℕ} {L : Language} {M : Type u_1} {s : Structure L M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LT L] [LT M] [Structure.LT L M] {e : Fin n → M} {ε : ξ → M} :
      (Eval s e ε) (ballLT t φ) ↔ ∀ x < Semiterm.val s e ε t, (Eval s (x :> e) ε) φ
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_bexLT {ξ : Type u_3} {n : ℕ} {L : Language} {M : Type u_1} {s : Structure L M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LT L] [LT M] [Structure.LT L M] {e : Fin n → M} {ε : ξ → M} :
      (Eval s e ε) (bexLT t φ) ↔ ∃ x < Semiterm.val s e ε t, (Eval s (x :> e) ε) φ
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_ballLE {ξ : Type u_3} {n : ℕ} {L : Language} {M : Type u_1} {s : Structure L M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LE L] [LE M] [Structure.LE L M] {e : Fin n → M} {ε : ξ → M} :
      (Eval s e ε) (ballLE t φ) ↔ ∀ x ≤ Semiterm.val s e ε t, (Eval s (x :> e) ε) φ
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_bexLE {ξ : Type u_3} {n : ℕ} {L : Language} {M : Type u_1} {s : Structure L M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LE L] [LE M] [Structure.LE L M] {e : Fin n → M} {ε : ξ → M} :
      (Eval s e ε) (bexLE t φ) ↔ ∃ x ≤ Semiterm.val s e ε t, (Eval s (x :> e) ε) φ
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_ballMem {ξ : Type u_3} {n : ℕ} {L : Language} {M : Type u_1} {s : Structure L M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.Mem L] [Membership M M] [Structure.Mem L M] {e : Fin n → M} {ε : ξ → M} :
      (Eval s e ε) (ballMem t φ) ↔ ∀ x ∈ Semiterm.val s e ε t, (Eval s (x :> e) ε) φ
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.eval_bexMem {ξ : Type u_3} {n : ℕ} {L : Language} {M : Type u_1} {s : Structure L M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.Mem L] [Membership M M] [Structure.Mem L M] {e : Fin n → M} {ε : ξ → M} :
      (Eval s e ε) (bexMem t φ) ↔ ∃ x ∈ Semiterm.val s e ε t, (Eval s (x :> e) ε) φ
      source
      @[reducible, inline]
      abbrev LO.FirstOrder.Semiterm.numeral {L : Language} [L.Zero] [L.One] [L.Add] {ξ : Type u_2} {n : ℕ} (k : ℕ) :
      Semiterm L ξ n
      Equations
      source
      instance LO.FirstOrder.Semiterm.instCoeNat {L : Language} [L.Zero] [L.One] [L.Add] {ξ : Type u_2} {n : ℕ} :
      Coe ℕ (Semiterm L ξ n)
      Equations