Foundation.FirstOrder.Basic.Semantics.Elementary

source

structure LO.FirstOrder.Structure.Hom (L : Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

Type (max u_2 u_3)

toFun : M₁ → M₂
func' {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : self.toFun (func f v) = func f (self.toFun ∘ v)
rel' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (self.toFun ∘ v)

Instances For

source

def LO.FirstOrder.Structure.«term_→ₛ[_]_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure LO.FirstOrder.Structure.Embedding (L : Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : Structure L M₁] [s₂ : Structure L M₂] extends M₁ →ₛ[L] M₂ :

Type (max u_2 u_3)

toFun : M₁ → M₂
func' {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : self.toFun (func f v) = func f (self.toFun ∘ v)
rel' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (self.toFun ∘ v)
toFun_inj : Function.Injective self.toFun
rel_inv' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r (self.toFun ∘ v) → rel r v

Instances For

source

def LO.FirstOrder.Structure.«term_↪ₛ[_]_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure LO.FirstOrder.Structure.Iso (L : Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : Structure L M₁] [s₂ : Structure L M₂] extends M₁ ↪ₛ[L] M₂ :

Type (max u_2 u_3)

toFun : M₁ → M₂
func' {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : self.toFun (func f v) = func f (self.toFun ∘ v)
rel' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (self.toFun ∘ v)
toFun_inj : Function.Injective self.toFun
rel_inv' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r (self.toFun ∘ v) → rel r v
toFun_bij : Function.Bijective self.toFun

Instances For

source

def LO.FirstOrder.Structure.«term_≃ₛ[_]_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure LO.FirstOrder.Structure.ClosedSubset (L : Language) (M : Type u_1) [s : Structure L M] :

Type u_1

domain : Set M
domain_closed {k : ℕ} (f : L.Func k) {v : Fin k → M} : (∀ (i : Fin k), v i ∈ self.domain) → func f v ∈ self.domain

Instances For

source

theorem LO.FirstOrder.Structure.ClosedSubset.ext {L : Language} {M : Type u_1} {s : Structure L M} {x y : ClosedSubset L M} (domain : x.domain = y.domain) :

x = y

source

class LO.FirstOrder.Structure.HomClass (F : Type u_5) (L : outParam Language) (M₁ : outParam (Type u_6)) (M₂ : outParam (Type u_7)) [s₁ : Structure L M₁] [s₂ : Structure L M₂] [FunLike F M₁ M₂] :

Prop

map_func (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : h (func f v) = func f (⇑h ∘ v)
map_rel (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (⇑h ∘ v)

Instances

source

class LO.FirstOrder.Structure.EmbeddingClass (F : Type u_5) (L : outParam Language) (M₁ : outParam (Type u_6)) (M₂ : outParam (Type u_7)) [s₁ : Structure L M₁] [s₂ : Structure L M₂] [FunLike F M₁ M₂] extends LO.FirstOrder.Structure.HomClass F L M₁ M₂ :

Prop

map_func (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : h (func f v) = func f (⇑h ∘ v)
map_rel (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (⇑h ∘ v)
map_inj (f : F) : Function.Injective ⇑f
map_rel_inv (f : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r (⇑f ∘ v) → rel r v

Instances

source

class LO.FirstOrder.Structure.IsoClass (F : Type u_5) (L : outParam Language) (M₁ : outParam (Type u_6)) (M₂ : outParam (Type u_7)) [s₁ : Structure L M₁] [s₂ : Structure L M₂] [FunLike F M₁ M₂] extends LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂ :

Prop

map_func (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : h (func f v) = func f (⇑h ∘ v)
map_rel (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (⇑h ∘ v)
map_inj (f : F) : Function.Injective ⇑f
map_rel_inv (f : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r (⇑f ∘ v) → rel r v
map_bij (f : F) : Function.Bijective ⇑f

Instances

source

instance LO.FirstOrder.Structure.instFunLikeHom {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

FunLike (M₁ →ₛ[L] M₂) M₁ M₂

Equations

LO.FirstOrder.Structure.instFunLikeHom = { coe := fun (φ : M₁ →ₛ[L] M₂) => φ.toFun, coe_injective' := ⋯ }

source

instance LO.FirstOrder.Structure.instHomClassHom {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

HomClass (M₁ →ₛ[L] M₂) L M₁ M₂

source

theorem LO.FirstOrder.Structure.Hom.ext {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] (φ ψ : M₁ →ₛ[L] M₂) (h : ∀ (x : M₁), φ x = ψ x) :

φ = ψ

source

theorem LO.FirstOrder.Structure.HomClass.ext {M₁ : Type u_2} {M₂ : Type u_3} {F : Type u_5} [FunLike F M₁ M₂] (φ ψ : F) (h : ∀ (x : M₁), φ x = ψ x) :

φ = ψ

source

theorem LO.FirstOrder.Structure.HomClass.func {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [HomClass F L M₁ M₂] (φ : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) :

φ (func f v) = func f (⇑φ ∘ v)

source

theorem LO.FirstOrder.Structure.HomClass.rel {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [HomClass F L M₁ M₂] (φ : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) :

rel r v → rel r (⇑φ ∘ v)

source

theorem LO.FirstOrder.Structure.HomClass.val_term {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [HomClass F L M₁ M₂] (φ : F) {n : ℕ} {ξ : Type u_6} (e : Fin n → M₁) (ε : ξ → M₁) (t : Semiterm L ξ n) :

φ (Semiterm.val s₁ e ε t) = Semiterm.val s₂ (⇑φ ∘ e) (⇑φ ∘ ε) t

source

instance LO.FirstOrder.Structure.instFunLikeEmbedding {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

FunLike (M₁ ↪ₛ[L] M₂) M₁ M₂

Equations

LO.FirstOrder.Structure.instFunLikeEmbedding = { coe := fun (φ : M₁ ↪ₛ[L] M₂) => φ.toFun, coe_injective' := ⋯ }

source

instance LO.FirstOrder.Structure.instEmbeddingClassEmbedding {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

EmbeddingClass (M₁ ↪ₛ[L] M₂) L M₁ M₂

source

theorem LO.FirstOrder.Structure.Embedding.ext {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] (φ ψ : M₁ ↪ₛ[L] M₂) (h : ∀ (x : M₁), φ x = ψ x) :

φ = ψ

source

def LO.FirstOrder.Structure.EmbeddingClass.toEmbedding {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [EmbeddingClass F L M₁ M₂] (φ : F) :

M₁ ↪ M₂

Equations

LO.FirstOrder.Structure.EmbeddingClass.toEmbedding φ = { toFun := ⇑φ, inj' := ⋯ }

Instances For

source

theorem LO.FirstOrder.Structure.EmbeddingClass.func {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [EmbeddingClass F L M₁ M₂] (φ : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) :

φ (func f v) = func f (⇑φ ∘ v)

source

theorem LO.FirstOrder.Structure.EmbeddingClass.rel {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [EmbeddingClass F L M₁ M₂] (φ : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) :

rel r (⇑φ ∘ v) ↔ rel r v

source

instance LO.FirstOrder.Structure.instFunLikeIso {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

FunLike (M₁ ≃ₛ[L] M₂) M₁ M₂

Equations

LO.FirstOrder.Structure.instFunLikeIso = { coe := fun (φ : M₁ ≃ₛ[L] M₂) => φ.toFun, coe_injective' := ⋯ }

source

instance LO.FirstOrder.Structure.instIsoClassIso {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

IsoClass (M₁ ≃ₛ[L] M₂) L M₁ M₂

source

theorem LO.FirstOrder.Structure.Iso.ext {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] (φ ψ : M₁ ≃ₛ[L] M₂) (h : ∀ (x : M₁), φ x = ψ x) :

φ = ψ

source

instance LO.FirstOrder.Structure.ClosedSubset.instSetLike {L : Language} {M : Type u_1} [s : Structure L M] :

SetLike (ClosedSubset L M) M

Equations

LO.FirstOrder.Structure.ClosedSubset.instSetLike = { coe := LO.FirstOrder.Structure.ClosedSubset.domain, coe_injective' := ⋯ }

source

theorem LO.FirstOrder.Structure.ClosedSubset.closed {L : Language} {M : Type u_1} [s : Structure L M] (u : ClosedSubset L M) {k : ℕ} (f : L.Func k) {v : Fin k → M} (hv : ∀ (i : Fin k), v i ∈ u) :

func f v ∈ u

source

instance LO.FirstOrder.Structure.ClosedSubset.toStructure {L : Language} {M : Type u_1} [s : Structure L M] (u : ClosedSubset L M) :

Structure L ↥u

Equations

One or more equations did not get rendered due to their size.

source

theorem LO.FirstOrder.Structure.ClosedSubset.func {L : Language} {M : Type u_1} [s : Structure L M] (u : ClosedSubset L M) {k : ℕ} (f : L.Func k) (v : Fin k → ↥u) :

↑(func f v) = func f fun (i : Fin k) => ↑(v i)

source

theorem LO.FirstOrder.Structure.ClosedSubset.rel {L : Language} {M : Type u_1} [s : Structure L M] (u : ClosedSubset L M) {k : ℕ} (r : L.Rel k) (v : Fin k → ↥u) :

rel r v ↔ rel r fun (i : Fin k) => ↑(v i)

source

def LO.FirstOrder.Structure.ClosedSubset.inclusion {L : Language} {M : Type u_1} [s : Structure L M] (u : ClosedSubset L M) :

↥u ↪ₛ[L] M

Equations

u.inclusion = { toFun := Subtype.val, func' := ⋯, rel' := ⋯, toFun_inj := ⋯, rel_inv' := ⋯ }

Instances For

source

theorem LO.FirstOrder.Semiformula.eval_hom_iff_of_open {ξ : Type u_6} {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [Structure.EmbeddingClass F L M₁ M₂] (Θ : F) {n : ℕ} {e₁ : Fin n → M₁} {ε₁ : ξ → M₁} {φ : Semiformula L ξ n} :

φ.Open → ((Eval s₁ e₁ ε₁) φ ↔ (Eval s₂ (⇑Θ ∘ e₁) (⇑Θ ∘ ε₁)) φ)

source

theorem LO.FirstOrder.Semiformula.eval_hom_univClosure {ξ : Type u_6} {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [Structure.EmbeddingClass F L M₁ M₂] (Θ : F) {n : ℕ} {ε₁ : ξ → M₁} {φ : Semiformula L ξ n} (hp : φ.Open) :

(Evalf s₂ (⇑Θ ∘ ε₁)) (∀* φ) → (Evalf s₁ ε₁) (∀* φ)

source

def LO.FirstOrder.Structure.ElementaryEquiv (L : Language) (M₁ : Type u_2) (M₂ : Type u_3) [Nonempty M₁] [Nonempty M₂] [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

Prop

Equations

(M₁ ≡ₑ[L] M₂) = ∀ (φ : LO.FirstOrder.SyntacticFormula L), M₁ ⊧ₘ φ ↔ M₂ ⊧ₘ φ

Instances For

source

def LO.FirstOrder.Structure.«term_≡ₑ[_]_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LO.FirstOrder.Structure.ElementaryEquiv.refl {L : Language} (M : Type u_5) [Nonempty M] [Structure L M] :

M ≡ₑ[L] M

source

theorem LO.FirstOrder.Structure.ElementaryEquiv.symm {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : Structure L M₁] [s₂ : Structure L M₂] :

(M₁ ≡ₑ[L] M₂) → M₂ ≡ₑ[L] M₁

source

theorem LO.FirstOrder.Structure.ElementaryEquiv.trans {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [Nonempty M₁] [Nonempty M₂] [Nonempty M₃] [s₁ : Structure L M₁] [s₂ : Structure L M₂] [s₃ : Structure L M₃] :

(M₁ ≡ₑ[L] M₂) → (M₂ ≡ₑ[L] M₃) → M₁ ≡ₑ[L] M₃

source

theorem LO.FirstOrder.Structure.ElementaryEquiv.models {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : Structure L M₁] [s₂ : Structure L M₂] (h : M₁ ≡ₑ[L] M₂) {φ : SyntacticFormula L} :

M₁ ⊧ₘ φ ↔ M₂ ⊧ₘ φ

source

theorem LO.FirstOrder.Structure.ElementaryEquiv.modelsTheory {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : Structure L M₁] [s₂ : Structure L M₂] (h : M₁ ≡ₑ[L] M₂) {T : Theory L} :

M₁ ⊧ₘ* T ↔ M₂ ⊧ₘ* T

source

theorem LO.FirstOrder.Structure.ElementaryEquiv.ofEquiv {L : Language} {M : Type u_1} [Nonempty M] [s : Structure L M] {N : Type u_5} [Nonempty N] (Θ : M ≃ N) :

M ≡ₑ[L] N