Foundation.FirstOrder.Tarski.Elementary

source

structure FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.Structure.«term_→ₛ[_]_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

structure FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.Structure.«term_↪ₛ[_]_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

structure FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.Structure.«term_≃ₛ[_]_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

structure FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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

theorem FFL.FirstOrder.Tarski.Structure.ClosedSubset.ext_iff {L : Language} {M : Type u_1} {s : Structure L M} {x y : ClosedSubset L M} :

x = y ↔ x.domain = y.domain

source

class FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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_reducible]

instance FFL.FirstOrder.Tarski.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

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

source

instance FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.Structure.Hom.ext_iff {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {φ ψ : M₁ →ₛ[L] M₂} :

φ = ψ ↔ ∀ (x : M₁), φ x = ψ x

source

theorem FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.Structure.HomClass.ext_iff {M₁ : Type u_2} {M₂ : Type u_3} {F : Type u_5} [FunLike F M₁ M₂] {φ ψ : F} :

φ = ψ ↔ ∀ (x : M₁), φ x = ψ x

source

theorem FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 e ε t) = Semiterm.val (⇑φ ∘ e) (⇑φ ∘ ε) t

source

@[instance_reducible]

instance FFL.FirstOrder.Tarski.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

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

source

instance FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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

theorem FFL.FirstOrder.Tarski.Structure.Embedding.ext_iff {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {φ ψ : M₁ ↪ₛ[L] M₂} :

φ = ψ ↔ ∀ (x : M₁), φ x = ψ x

source

def FFL.FirstOrder.Tarski.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

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

Instances For

source

theorem FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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_reducible]

instance FFL.FirstOrder.Tarski.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

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

source

instance FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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

theorem FFL.FirstOrder.Tarski.Structure.Iso.ext_iff {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {φ ψ : M₁ ≃ₛ[L] M₂} :

φ = ψ ↔ ∀ (x : M₁), φ x = ψ x

source

@[instance_reducible]

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

SetLike (ClosedSubset L M) M

Equations

FFL.FirstOrder.Tarski.Structure.ClosedSubset.instSetLike = { coe := FFL.FirstOrder.Tarski.Structure.ClosedSubset.domain, coe_injective := ⋯ }

source

theorem FFL.FirstOrder.Tarski.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_reducible]

instance FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Semiformula.eval_hom_iff_of_open {ξ : Type u_6} {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Tarski.Structure L M₁] [s₂ : Tarski.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [Tarski.Structure.EmbeddingClass F L M₁ M₂] (Θ : F) {n : ℕ} {e₁ : Fin n → M₁} {ε₁ : ξ → M₁} {φ : Semiformula L ξ n} (h : φ.Open) :

(Eval e₁ ε₁) φ ↔ (Eval (⇑Θ ∘ e₁) (⇑Θ ∘ ε₁)) φ

source

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

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

source

class FFL.FirstOrder.Tarski.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

models {φ : Sentence L} : M₁↓[L] ⊧ φ ↔ M₂↓[L] ⊧ φ

Instances

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

instance FFL.FirstOrder.Tarski.Structure.ElementaryEquiv.refl {L : Language} (M : Type u_5) [Nonempty M] [Structure L M] :

M ≡ₑ[L] M

source

theorem FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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 FFL.FirstOrder.Tarski.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₁↓[L] ⊧* T ↔ M₂↓[L] ⊧* T

source

theorem FFL.FirstOrder.Tarski.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₂] [M₁ ≡ₑ[L] M₂] (T : Theory L) [h : M₂↓[L] ⊧* T] :

M₁↓[L] ⊧* T

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.Structure.ElementaryEquiv.val_eq_of_equiv {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {ξ : Type u_5} {n : ℕ} {f₁ : ξ → M₁} {f₂ : ξ → M₂} {b₁ : Fin n → M₁} {b₂ : Fin n → M₂} (I : M₁ ≃ M₂) (hf : ∀ (x : ξ), I (f₁ x) = f₂ x) (hb : ∀ (x : Fin n), I (b₁ x) = b₂ x) (hfunc : ∀ {k : ℕ} (f : L.Func k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → I (func f v₁) = func f v₂) (t : Semiterm L ξ n) :

I (Semiterm.val b₁ f₁ t) = Semiterm.val b₂ f₂ t

source

theorem FFL.FirstOrder.Tarski.Structure.ElementaryEquiv.eval_iff_of_equiv {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {ξ : Type u_5} {n : ℕ} {f₁ : ξ → M₁} {f₂ : ξ → M₂} {b₁ : Fin n → M₁} {b₂ : Fin n → M₂} (I : M₁ ≃ M₂) (hf : ∀ (x : ξ), I (f₁ x) = f₂ x) (hb : ∀ (x : Fin n), I (b₁ x) = b₂ x) (hrel : ∀ {k : ℕ} (R : L.Rel k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → (rel R v₁ ↔ rel R v₂)) (hfunc : ∀ {k : ℕ} (f : L.Func k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → I (func f v₁) = func f v₂) (φ : Semiformula L ξ n) :

(Semiformula.Eval b₁ f₁) φ ↔ (Semiformula.Eval b₂ f₂) φ

source

theorem FFL.FirstOrder.Tarski.Structure.ElementaryEquiv.of_equiv {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : Structure L M₁] [s₂ : Structure L M₂] (I : M₁ ≃ M₂) (hrel : ∀ {k : ℕ} (R : L.Rel k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → (rel R v₁ ↔ rel R v₂)) (hfunc : ∀ {k : ℕ} (f : L.Func k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → I (func f v₁) = func f v₂) :

M₁ ≡ₑ[L] M₂