Equations
- Matrix.iget v x = if h : x < k then v ⟨x, h⟩ else default
Instances For
class
LO.FirstOrder.Theory.Sub
{L : LO.FirstOrder.Language}
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
:
- sub : T ⊆ U
Instances
theorem
LO.FirstOrder.Theory.Sub.sub
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{U : LO.FirstOrder.Theory L}
[self : T.Sub U]
:
T ⊆ U
inductive
LO.FirstOrder.Theory.eqAxiom
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
:
- refl: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L], 𝐄𝐐 (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)
- symm: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L], 𝐄𝐐 (“(!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) → !!(LO.FirstOrder.Semiterm.fvar 1) = !!(LO.FirstOrder.Semiterm.fvar 0))”)
- trans: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L], 𝐄𝐐 (“(!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) → (!!(LO.FirstOrder.Semiterm.fvar 1) = !!(LO.FirstOrder.Semiterm.fvar 2) → !!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 2)))”)
- funcExt: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k), 𝐄𝐐 (“(!(Matrix.conj fun (i : Fin k) => “!!(LO.FirstOrder.Semiterm.fvar ↑i) = !!(LO.FirstOrder.Semiterm.fvar (k + ↑i))”) → !!(LO.FirstOrder.Semiterm.func f fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar ↑i) = !!(LO.FirstOrder.Semiterm.func f fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar (k + ↑i)))”)
- relExt: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k), 𝐄𝐐 ((Matrix.conj fun (i : Fin k) => “!!(LO.FirstOrder.Semiterm.fvar ↑i) = !!(LO.FirstOrder.Semiterm.fvar (k + ↑i))”) ➝ (LO.FirstOrder.Semiformula.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar ↑i) ➝ LO.FirstOrder.Semiformula.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar (k + ↑i))
Instances For
Equations
- LO.FirstOrder.Theory.«term𝐄𝐐» = Lean.ParserDescr.node `LO.FirstOrder.Theory.term𝐄𝐐 1024 (Lean.ParserDescr.symbol "𝐄𝐐")
Instances For
@[simp]
theorem
LO.FirstOrder.Structure.Eq.models_eqAxiom
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
:
instance
LO.FirstOrder.Structure.Eq.models_eqAxiom'
(L : LO.FirstOrder.Language)
[LO.FirstOrder.Semiformula.Operator.Eq L]
(M : Type u)
[Nonempty M]
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
:
Equations
- ⋯ = ⋯
def
LO.FirstOrder.Structure.Eq.eqv
(L : LO.FirstOrder.Language)
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[LO.FirstOrder.Structure L M]
(a : M)
(b : M)
:
Equations
- LO.FirstOrder.Structure.Eq.eqv L a b = op(=).val ![a, b]
Instances For
theorem
LO.FirstOrder.Structure.Eq.eqv_refl
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
(a : M)
:
theorem
LO.FirstOrder.Structure.Eq.eqv_symm
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
{a : M}
{b : M}
:
LO.FirstOrder.Structure.Eq.eqv L a b → LO.FirstOrder.Structure.Eq.eqv L b a
theorem
LO.FirstOrder.Structure.Eq.eqv_trans
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
{a : M}
{b : M}
{c : M}
:
LO.FirstOrder.Structure.Eq.eqv L a b → LO.FirstOrder.Structure.Eq.eqv L b c → LO.FirstOrder.Structure.Eq.eqv L a c
theorem
LO.FirstOrder.Structure.Eq.eqv_funcExt
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
{k : ℕ}
(f : L.Func k)
{v : Fin k → M}
{w : Fin k → M}
(h : ∀ (i : Fin k), LO.FirstOrder.Structure.Eq.eqv L (v i) (w i))
:
theorem
LO.FirstOrder.Structure.Eq.eqv_relExt_aux
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
{k : ℕ}
(r : L.Rel k)
{v : Fin k → M}
{w : Fin k → M}
(h : ∀ (i : Fin k), LO.FirstOrder.Structure.Eq.eqv L (v i) (w i))
:
theorem
LO.FirstOrder.Structure.Eq.eqv_relExt
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
{k : ℕ}
(r : L.Rel k)
{v : Fin k → M}
{w : Fin k → M}
(h : ∀ (i : Fin k), LO.FirstOrder.Structure.Eq.eqv L (v i) (w i))
:
theorem
LO.FirstOrder.Structure.Eq.eqv_equivalence
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
:
def
LO.FirstOrder.Structure.Eq.eqvSetoid
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
:
Setoid M
Equations
- LO.FirstOrder.Structure.Eq.eqvSetoid H = { r := LO.FirstOrder.Structure.Eq.eqv L, iseqv := ⋯ }
Instances For
def
LO.FirstOrder.Structure.Eq.QuotEq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
:
Type u
Instances For
instance
LO.FirstOrder.Structure.Eq.QuotEq.inhabited
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
:
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Structure.Eq.of_eq_of
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
{a : M}
{b : M}
:
⟦a⟧ = ⟦b⟧ ↔ LO.FirstOrder.Structure.Eq.eqv L a b
def
LO.FirstOrder.Structure.Eq.QuotEq.func
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
⦃k : ℕ⦄
(f : L.Func k)
(v : Fin k → LO.FirstOrder.Structure.Eq.QuotEq H)
:
Equations
- LO.FirstOrder.Structure.Eq.QuotEq.func H f v = Quotient.liftVec (fun (x : Fin k → M) => ⟦LO.FirstOrder.Structure.func f x⟧) ⋯ v
Instances For
def
LO.FirstOrder.Structure.Eq.QuotEq.rel
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
⦃k : ℕ⦄
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Structure.Eq.QuotEq H)
:
Equations
Instances For
instance
LO.FirstOrder.Structure.Eq.QuotEq.struc
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
:
Equations
- LO.FirstOrder.Structure.Eq.QuotEq.struc = { func := LO.FirstOrder.Structure.Eq.QuotEq.func H, rel := LO.FirstOrder.Structure.Eq.QuotEq.rel H }
theorem
LO.FirstOrder.Structure.Eq.QuotEq.funk_mk
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
{k : ℕ}
(f : L.Func k)
(v : Fin k → M)
:
(LO.FirstOrder.Structure.func f fun (i : Fin k) => ⟦v i⟧) = ⟦LO.FirstOrder.Structure.func f v⟧
theorem
LO.FirstOrder.Structure.Eq.QuotEq.rel_mk
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
{k : ℕ}
(r : L.Rel k)
(v : Fin k → M)
:
(LO.FirstOrder.Structure.rel r fun (i : Fin k) => ⟦v i⟧) ↔ LO.FirstOrder.Structure.rel r v
theorem
LO.FirstOrder.Structure.Eq.QuotEq.val_mk
{L : LO.FirstOrder.Language}
{μ : Type u_1}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
{n : ℕ}
{e : Fin n → M}
{ε : μ → M}
(t : LO.FirstOrder.Semiterm L μ n)
:
LO.FirstOrder.Semiterm.valm (LO.FirstOrder.Structure.Eq.QuotEq H) (fun (i : Fin n) => ⟦e i⟧) (fun (i : μ) => ⟦ε i⟧) t = ⟦LO.FirstOrder.Semiterm.valm M e ε t⟧
theorem
LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
{L : LO.FirstOrder.Language}
{μ : Type u_1}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
{n : ℕ}
{e : Fin n → M}
{ε : μ → M}
{p : LO.FirstOrder.Semiformula L μ n}
:
(LO.FirstOrder.Semiformula.Evalm (LO.FirstOrder.Structure.Eq.QuotEq H) (fun (i : Fin n) => ⟦e i⟧) fun (i : μ) => ⟦ε i⟧)
p ↔ (LO.FirstOrder.Semiformula.Evalm M e ε) p
theorem
LO.FirstOrder.Structure.Eq.QuotEq.eval_mk₀
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
{ξ : Type u_2}
{ε : ξ → M}
{p : LO.FirstOrder.Formula L ξ}
:
(LO.FirstOrder.Semiformula.Evalfm (LO.FirstOrder.Structure.Eq.QuotEq H) fun (i : ξ) => ⟦ε i⟧) p ↔ (LO.FirstOrder.Semiformula.Evalfm M ε) p
theorem
LO.FirstOrder.Structure.Eq.QuotEq.models_iff
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
{p : LO.FirstOrder.SyntacticFormula L}
:
LO.FirstOrder.Structure.Eq.QuotEq H ⊧ₘ p ↔ M ⊧ₘ p
theorem
LO.FirstOrder.Structure.Eq.QuotEq.elementaryEquiv
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(H : M ⊧ₘ* 𝐄𝐐)
:
theorem
LO.FirstOrder.Structure.Eq.QuotEq.rel_eq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
(a : LO.FirstOrder.Structure.Eq.QuotEq H)
(b : LO.FirstOrder.Structure.Eq.QuotEq H)
:
instance
LO.FirstOrder.Structure.Eq.QuotEq.structureEq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u}
[Nonempty M]
[LO.FirstOrder.Structure L M]
{H : M ⊧ₘ* 𝐄𝐐}
:
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.consequence_iff_eq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{p : LO.FirstOrder.SyntacticFormula L}
:
T ⊨[LO.FirstOrder.Struc L] p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.Eq L M],
M ⊧ₘ* T → M ⊧ₘ p
theorem
LO.FirstOrder.consequence_iff_eq'
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
{p : LO.FirstOrder.SyntacticFormula L}
:
T ⊨[LO.FirstOrder.Struc L] p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.Eq L M]
[inst_3 : M ⊧ₘ* T], M ⊧ₘ p
theorem
LO.FirstOrder.satisfiable_iff_eq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
:
LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : LO.FirstOrder.Structure L M) (_ : LO.FirstOrder.Structure.Eq L M), M ⊧ₘ* T
def
LO.FirstOrder.ModelOfSatEq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
:
Type v
Equations
- LO.FirstOrder.ModelOfSatEq sat = let_fun H := ⋯; LO.FirstOrder.Structure.Eq.QuotEq H
Instances For
noncomputable instance
LO.FirstOrder.ModelOfSatEq.instNonempty
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
:
Equations
- ⋯ = ⋯
noncomputable instance
LO.FirstOrder.ModelOfSatEq.struc
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
:
Equations
- LO.FirstOrder.ModelOfSatEq.struc sat = LO.FirstOrder.Structure.Eq.QuotEq.struc
noncomputable instance
LO.FirstOrder.ModelOfSatEq.instEq
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
:
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.ModelOfSatEq.models
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
:
instance
LO.FirstOrder.ModelOfSatEq.mod
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
:
Equations
- ⋯ = ⋯
noncomputable instance
LO.FirstOrder.ModelOfSatEq.instZeroOfZero
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.Zero L]
:
Equations
- LO.FirstOrder.ModelOfSatEq.instZeroOfZero sat = { zero := LO.FirstOrder.Semiterm.Operator.val op(0) ![] }
instance
LO.FirstOrder.ModelOfSatEq.strucZero
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.Zero L]
:
Equations
- ⋯ = ⋯
noncomputable instance
LO.FirstOrder.ModelOfSatEq.instOneOfOne
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.One L]
:
Equations
- LO.FirstOrder.ModelOfSatEq.instOneOfOne sat = { one := LO.FirstOrder.Semiterm.Operator.val op(1) ![] }
instance
LO.FirstOrder.ModelOfSatEq.instOne
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.One L]
:
Equations
- ⋯ = ⋯
noncomputable instance
LO.FirstOrder.ModelOfSatEq.instAddOfAdd
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.Add L]
:
Equations
- LO.FirstOrder.ModelOfSatEq.instAddOfAdd sat = { add := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(+).val ![x, y] }
instance
LO.FirstOrder.ModelOfSatEq.instAdd
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.Add L]
:
Equations
- ⋯ = ⋯
noncomputable instance
LO.FirstOrder.ModelOfSatEq.instMulOfMul
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.Mul L]
:
Equations
- LO.FirstOrder.ModelOfSatEq.instMulOfMul sat = { mul := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(*).val ![x, y] }
instance
LO.FirstOrder.ModelOfSatEq.instMul
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiterm.Operator.Mul L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.ModelOfSatEq.instLTOfLT
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiformula.Operator.LT L]
:
LT (LO.FirstOrder.ModelOfSatEq sat)
Equations
- LO.FirstOrder.ModelOfSatEq.instLTOfLT sat = { lt := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(<).val ![x, y] }
instance
LO.FirstOrder.ModelOfSatEq.instLT
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiformula.Operator.LT L]
:
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.ModelOfSatEq.instMembershipOfMem
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiformula.Operator.Mem L]
:
Equations
- LO.FirstOrder.ModelOfSatEq.instMembershipOfMem sat = { mem := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(∈).val ![x, y] }
instance
LO.FirstOrder.ModelOfSatEq.instMem
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T)
[LO.FirstOrder.Semiformula.Operator.Mem L]
:
Equations
- ⋯ = ⋯
def
LO.FirstOrder.Semiformula.existsUnique
{L : LO.FirstOrder.Language}
{μ : Type u_1}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{n : ℕ}
(p : LO.FirstOrder.Semiformula L μ (n + 1))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.FirstOrder.Semiformula.eval_existsUnique
{L : LO.FirstOrder.Language}
{μ : Type u_1}
[LO.FirstOrder.Semiformula.Operator.Eq L]
{M : Type u_2}
[s : LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Eq L M]
{n : ℕ}
{e : Fin n → M}
{ε : μ → M}
{p : LO.FirstOrder.Semiformula L μ (n + 1)}
:
(LO.FirstOrder.Semiformula.Eval s e ε) (∃'! p) ↔ ∃! x : M, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.