- intro : M
Instances For
Equations
- LO.FirstOrder.Structure.Model.equiv L M = { toFun := fun (x : M) => { intro := x }, invFun := LO.FirstOrder.Structure.Model.intro, left_inv := ⋯, right_inv := ⋯ }
Instances For
instance
LO.FirstOrder.Structure.Model.inst
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
:
Equations
- LO.FirstOrder.Structure.Model.inst = LO.FirstOrder.Structure.ofEquiv (LO.FirstOrder.Structure.Model.equiv L M)
instance
LO.FirstOrder.Structure.Model.instNonempty
{L : LO.FirstOrder.Language}
{M : Type u_1}
[h : Nonempty M]
:
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Structure.Model.elementaryEquiv
(L : LO.FirstOrder.Language)
(M : Type u_1)
[Nonempty M]
[LO.FirstOrder.Structure L M]
:
instance
LO.FirstOrder.Structure.Model.instZeroOfZero
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Zero L]
:
Equations
- LO.FirstOrder.Structure.Model.instZeroOfZero = { zero := LO.FirstOrder.Semiterm.Operator.val op(0) ![] }
instance
LO.FirstOrder.Structure.Model.instZero
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Zero L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instOneOfOne
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.One L]
:
Equations
- LO.FirstOrder.Structure.Model.instOneOfOne = { one := LO.FirstOrder.Semiterm.Operator.val op(1) ![] }
instance
LO.FirstOrder.Structure.Model.instOne
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.One L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instAddOfAdd
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Add L]
:
Equations
- LO.FirstOrder.Structure.Model.instAddOfAdd = { add := fun (x y : LO.FirstOrder.Structure.Model L M) => op(+).val ![x, y] }
instance
LO.FirstOrder.Structure.Model.instAdd
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Add L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instMulOfMul
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Mul L]
:
Equations
- LO.FirstOrder.Structure.Model.instMulOfMul = { mul := fun (x y : LO.FirstOrder.Structure.Model L M) => op(*).val ![x, y] }
instance
LO.FirstOrder.Structure.Model.instMul
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Mul L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instExpOfExp
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Exp L]
:
Equations
- LO.FirstOrder.Structure.Model.instExpOfExp = { exp := fun (x : LO.FirstOrder.Structure.Model L M) => LO.FirstOrder.Semiterm.Operator.Exp.exp.val ![x] }
instance
LO.FirstOrder.Structure.Model.instExp
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiterm.Operator.Exp L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instEq
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiformula.Operator.Eq L]
[LO.FirstOrder.Structure.Eq L M]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instLTOfLT
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiformula.Operator.LT L]
:
Equations
- LO.FirstOrder.Structure.Model.instLTOfLT = { lt := fun (x y : LO.FirstOrder.Structure.Model L M) => op(<).val ![x, y] }
instance
LO.FirstOrder.Structure.Model.instLT
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiformula.Operator.LT L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.Model.instMembershipOfMem
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiformula.Operator.Mem L]
:
Equations
- LO.FirstOrder.Structure.Model.instMembershipOfMem = { mem := fun (x y : LO.FirstOrder.Structure.Model L M) => op(∈).val ![x, y] }
instance
LO.FirstOrder.Structure.Model.instMem
{L : LO.FirstOrder.Language}
{M : Type u_2}
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Semiformula.Operator.Mem L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Structure.add
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
(M : Type u_1)
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
:
LO.FirstOrder.Structure (L₁.add L₂) M
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LO.FirstOrder.Structure.func_sigma_inl
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{k : ℕ}
(f : L₁.Func k)
(v : Fin k → M)
:
@[simp]
theorem
LO.FirstOrder.Structure.func_sigma_inr
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{k : ℕ}
(f : L₂.Func k)
(v : Fin k → M)
:
@[simp]
theorem
LO.FirstOrder.Structure.rel_sigma_inl
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{k : ℕ}
(r : L₁.Rel k)
(v : Fin k → M)
:
@[simp]
theorem
LO.FirstOrder.Structure.rel_sigma_inr
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{k : ℕ}
(r : L₂.Rel k)
(v : Fin k → M)
:
@[simp]
theorem
LO.FirstOrder.Structure.val_lMap_add₁
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{μ : Type u_2}
{n : ℕ}
(t : LO.FirstOrder.Semiterm L₁ μ n)
(e : Fin n → M)
(ε : μ → M)
:
LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.add L₁ L₂ M) e ε
(LO.FirstOrder.Semiterm.lMap (LO.FirstOrder.Language.Hom.add₁ L₁ L₂) t) = LO.FirstOrder.Semiterm.val str₁ e ε t
@[simp]
theorem
LO.FirstOrder.Structure.val_lMap_add₂
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{μ : Type u_2}
{n : ℕ}
(t : LO.FirstOrder.Semiterm L₂ μ n)
(e : Fin n → M)
(ε : μ → M)
:
LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.add L₁ L₂ M) e ε
(LO.FirstOrder.Semiterm.lMap (LO.FirstOrder.Language.Hom.add₂ L₁ L₂) t) = LO.FirstOrder.Semiterm.val str₂ e ε t
@[simp]
theorem
LO.FirstOrder.Structure.eval_lMap_add₁
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{μ : Type u_2}
{n : ℕ}
(p : LO.FirstOrder.Semiformula L₁ μ n)
(e : Fin n → M)
(ε : μ → M)
:
(LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.add L₁ L₂ M) e ε)
((LO.FirstOrder.Semiformula.lMap (LO.FirstOrder.Language.Hom.add₁ L₁ L₂)) p) ↔ (LO.FirstOrder.Semiformula.Eval str₁ e ε) p
@[simp]
theorem
LO.FirstOrder.Structure.eval_lMap_add₂
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{M : Type u_1}
[str₁ : LO.FirstOrder.Structure L₁ M]
[str₂ : LO.FirstOrder.Structure L₂ M]
{μ : Type u_2}
{n : ℕ}
(p : LO.FirstOrder.Semiformula L₂ μ n)
(e : Fin n → M)
(ε : μ → M)
:
(LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.add L₁ L₂ M) e ε)
((LO.FirstOrder.Semiformula.lMap (LO.FirstOrder.Language.Hom.add₂ L₁ L₂)) p) ↔ (LO.FirstOrder.Semiformula.Eval str₂ e ε) p
instance
LO.FirstOrder.Structure.sigma
{ι : Type u_2}
(L : ι → LO.FirstOrder.Language)
(M : Type u_1)
[str : (i : ι) → LO.FirstOrder.Structure (L i) M]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LO.FirstOrder.Structure.func_sigma
{ι : Type u_3}
(L : ι → LO.FirstOrder.Language)
(M : Type u_1)
[str : (i : ι) → LO.FirstOrder.Structure (L i) M]
{i : ι}
{k : ℕ}
(f : (L i).Func k)
(v : Fin k → M)
:
LO.FirstOrder.Structure.func ⟨i, f⟩ v = LO.FirstOrder.Structure.func f v
@[simp]
theorem
LO.FirstOrder.Structure.rel_sigma
{ι : Type u_3}
(L : ι → LO.FirstOrder.Language)
(M : Type u_1)
[str : (i : ι) → LO.FirstOrder.Structure (L i) M]
{i : ι}
{k : ℕ}
(r : (L i).Rel k)
(v : Fin k → M)
:
LO.FirstOrder.Structure.rel ⟨i, r⟩ v ↔ LO.FirstOrder.Structure.rel r v
@[simp]
theorem
LO.FirstOrder.Structure.val_lMap_sigma
{ι : Type u_4}
(L : ι → LO.FirstOrder.Language)
(M : Type u_1)
[str : (i : ι) → LO.FirstOrder.Structure (L i) M]
{i : ι}
{μ : Type u_2}
{n : ℕ}
(t : LO.FirstOrder.Semiterm (L i) μ n)
(e : Fin n → M)
(ε : μ → M)
:
LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.sigma L M) e ε
(LO.FirstOrder.Semiterm.lMap (LO.FirstOrder.Language.Hom.sigma L i) t) = LO.FirstOrder.Semiterm.val (str i) e ε t
@[simp]
theorem
LO.FirstOrder.Structure.eval_lMap_sigma
{ι : Type u_4}
(L : ι → LO.FirstOrder.Language)
(M : Type u_1)
[str : (i : ι) → LO.FirstOrder.Structure (L i) M]
{i : ι}
{μ : Type u_2}
{n : ℕ}
(p : LO.FirstOrder.Semiformula (L i) μ n)
(e : Fin n → M)
(ε : μ → M)
:
(LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.sigma L M) e ε)
((LO.FirstOrder.Semiformula.lMap (LO.FirstOrder.Language.Hom.sigma L i)) p) ↔ (LO.FirstOrder.Semiformula.Eval (str i) e ε) p
instance
LO.FirstOrder.instStructureULift
{L : LO.FirstOrder.Language}
{M : Type v}
[LO.FirstOrder.Structure L M]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LO.FirstOrder.Structure.func_uLift
{L : LO.FirstOrder.Language}
{M : Type v}
[LO.FirstOrder.Structure L M]
{k : ℕ}
(f : L.Func k)
(v : Fin k → ULift.{v', v} M)
:
LO.FirstOrder.Structure.func f v = { down := LO.FirstOrder.Structure.func f fun (i : Fin k) => (v i).down }
@[simp]
theorem
LO.FirstOrder.Structure.rel_uLift
{L : LO.FirstOrder.Language}
{M : Type v}
[LO.FirstOrder.Structure L M]
{k : ℕ}
(r : L.Rel k)
(v : Fin k → ULift.{v', v} M)
:
LO.FirstOrder.Structure.rel r v = LO.FirstOrder.Structure.rel r fun (i : Fin k) => (v i).down
theorem
LO.FirstOrder.Semiterm.valm_uLift
{L : LO.FirstOrder.Language}
{M : Type v}
[LO.FirstOrder.Structure L M]
{n : ℕ}
{ξ : Type u_1}
{e : Fin n → ULift.{v', v} M}
{ε : ξ → ULift.{v', v} M}
{t : LO.FirstOrder.Semiterm L ξ n}
:
LO.FirstOrder.Semiterm.valm (ULift.{v', v} M) e ε t = { down := LO.FirstOrder.Semiterm.valm M (fun (i : Fin n) => (e i).down) (fun (i : ξ) => (ε i).down) t }
theorem
LO.FirstOrder.Semiformula.evalm_uLift
{L : LO.FirstOrder.Language}
{M : Type v}
[LO.FirstOrder.Structure L M]
{n : ℕ}
{ξ : Type u_1}
{e : Fin n → ULift.{v', v} M}
{ε : ξ → ULift.{v', v} M}
{p : LO.FirstOrder.Semiformula L ξ n}
:
(LO.FirstOrder.Semiformula.Evalm (ULift.{v', v} M) e ε) p ↔ (LO.FirstOrder.Semiformula.Evalm M (fun (i : Fin n) => (e i).down) fun (i : ξ) => (ε i).down) p
theorem
LO.FirstOrder.uLift_elementaryEquiv
(L : LO.FirstOrder.Language)
(M : Type v)
[LO.FirstOrder.Structure L M]
[Nonempty M]
:
ULift.{v', v} M ≡ₑ[L] M