First-Order Substructures #

This file defines substructures of first-order structures in a similar manner to the various substructures appearing in the algebra library.

Main Definitions #

A FirstOrder.Language.Substructure is defined so that L.Substructure M is the type of all substructures of the L-structure M.
FirstOrder.Language.Substructure.closure is defined so that if s : Set M, closure L s is the least substructure of M containing s.
FirstOrder.Language.Substructure.comap is defined so that s.comap f is the preimage of the substructure s under the homomorphism f, as a substructure.
FirstOrder.Language.Substructure.map is defined so that s.map f is the image of the substructure s under the homomorphism f, as a substructure.
FirstOrder.Language.Hom.range is defined so that f.range is the range of the homomorphism f, as a substructure.
FirstOrder.Language.Hom.domRestrict and FirstOrder.Language.Hom.codRestrict restrict the domain and codomain respectively of first-order homomorphisms to substructures.
FirstOrder.Language.Embedding.domRestrict and FirstOrder.Language.Embedding.codRestrict restrict the domain and codomain respectively of first-order embeddings to substructures.
FirstOrder.Language.Substructure.inclusion is the inclusion embedding between substructures.
FirstOrder.Language.Substructure.PartialEquiv is defined so that PartialEquiv L M N is the type of equivalences between substructures of M and N.

Main Results #

L.Substructure M forms a CompleteLattice.

source

def FirstOrder.Language.ClosedUnder {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (f : L.Functions n) (s : Set M) :

Prop

Indicates that a set in a given structure is a closed under a function symbol.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.closedUnder_univ (L : Language) {M : Type w} [L.Structure M] {n : ℕ} (f : L.Functions n) :

ClosedUnder f Set.univ

source

theorem FirstOrder.Language.ClosedUnder.inter {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {f : L.Functions n} {s t : Set M} (hs : ClosedUnder f s) (ht : ClosedUnder f t) :

ClosedUnder f (s ∩ t)

source

theorem FirstOrder.Language.ClosedUnder.inf {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {f : L.Functions n} {s t : Set M} (hs : ClosedUnder f s) (ht : ClosedUnder f t) :

ClosedUnder f (s ⊓ t)

source

theorem FirstOrder.Language.ClosedUnder.sInf {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {f : L.Functions n} {S : Set (Set M)} (hS : ∀ s ∈ S, ClosedUnder f s) :

ClosedUnder f (InfSet.sInf S)

source

structure FirstOrder.Language.Substructure (L : Language) (M : Type w) [L.Structure M] :

Type w

A substructure of a structure M is a set closed under application of function symbols.

carrier : Set M
The underlying set of this substructure
fun_mem {n : ℕ} (f : L.Functions n) : ClosedUnder f ↑self

Instances For

source

instance FirstOrder.Language.Substructure.instSetLike {L : Language} {M : Type w} [L.Structure M] :

SetLike (L.Substructure M) M

Equations

source

def FirstOrder.Language.Substructure.Simps.coe {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

Set M

See Note [custom simps projection]

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_carrier {L : Language} {M : Type w} [L.Structure M] {s : L.Substructure M} {x : M} :

x ∈ ↑s ↔ x ∈ s

source

theorem FirstOrder.Language.Substructure.ext {L : Language} {M : Type w} [L.Structure M] {S T : L.Substructure M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :

S = T

Two substructures are equal if they have the same elements.

source

theorem FirstOrder.Language.Substructure.ext_iff {L : Language} {M : Type w} [L.Structure M] {S T : L.Substructure M} :

S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T

source

def FirstOrder.Language.Substructure.copy {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) (s : Set M) (hs : s = ↑S) :

L.Substructure M

Copy a substructure replacing carrier with a set that is equal to it.

Equations

Instances For

source

theorem FirstOrder.Language.Term.realize_mem {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {α : Type u_3} (t : L.Term α) (xs : α → M) (h : ∀ (a : α), xs a ∈ S) :

realize xs t ∈ S

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_copy {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = ↑S) :

↑(S.copy s hs) = s

source

theorem FirstOrder.Language.Substructure.copy_eq {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = ↑S) :

S.copy s hs = S

source

theorem FirstOrder.Language.Substructure.constants_mem {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} (c : L.Constants) :

↑c ∈ S

source

instance FirstOrder.Language.Substructure.instTop {L : Language} {M : Type w} [L.Structure M] :

Top (L.Substructure M)

The substructure M of the structure M.

Equations

source

instance FirstOrder.Language.Substructure.instInhabited {L : Language} {M : Type w} [L.Structure M] :

Inhabited (L.Substructure M)

Equations

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_top {L : Language} {M : Type w} [L.Structure M] (x : M) :

x ∈ ⊤

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_top {L : Language} {M : Type w} [L.Structure M] :

↑⊤ = Set.univ

source

instance FirstOrder.Language.Substructure.instInf {L : Language} {M : Type w} [L.Structure M] :

Min (L.Substructure M)

The inf of two substructures is their intersection.

Equations

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_inf {L : Language} {M : Type w} [L.Structure M] (p p' : L.Substructure M) :

↑(p ⊓ p') = ↑p ∩ ↑p'

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_inf {L : Language} {M : Type w} [L.Structure M] {p p' : L.Substructure M} {x : M} :

x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

source

instance FirstOrder.Language.Substructure.instInfSet {L : Language} {M : Type w} [L.Structure M] :

InfSet (L.Substructure M)

Equations

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_sInf {L : Language} {M : Type w} [L.Structure M] (S : Set (L.Substructure M)) :

↑(sInf S) = ⋂ s ∈ S, ↑s

source

theorem FirstOrder.Language.Substructure.mem_sInf {L : Language} {M : Type w} [L.Structure M] {S : Set (L.Substructure M)} {x : M} :

x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

source

theorem FirstOrder.Language.Substructure.mem_iInf {L : Language} {M : Type w} [L.Structure M] {ι : Sort u_3} {S : ι → L.Substructure M} {x : M} :

x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_iInf {L : Language} {M : Type w} [L.Structure M] {ι : Sort u_3} {S : ι → L.Substructure M} :

↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

source

instance FirstOrder.Language.Substructure.instCompleteLattice {L : Language} {M : Type w} [L.Structure M] :

CompleteLattice (L.Substructure M)

Substructures of a structure form a complete lattice.

Equations

source

def FirstOrder.Language.Substructure.closure (L : Language) {M : Type w} [L.Structure M] :

LowerAdjoint SetLike.coe

The L.Substructure generated by a set.

Equations

Instances For

source

theorem FirstOrder.Language.Substructure.mem_closure {L : Language} {M : Type w} [L.Structure M] {s : Set M} {x : M} :

x ∈ (closure L).toFun s ↔ ∀ (S : L.Substructure M), s ⊆ ↑S → x ∈ S

source

@[simp]

theorem FirstOrder.Language.Substructure.subset_closure {L : Language} {M : Type w} [L.Structure M] {s : Set M} :

s ⊆ ↑((closure L).toFun s)

The substructure generated by a set includes the set.

source

theorem FirstOrder.Language.Substructure.notMem_of_notMem_closure {L : Language} {M : Type w} [L.Structure M] {s : Set M} {P : M} (hP : P ∉ (closure L).toFun s) :

P ∉ s

source

@[deprecated FirstOrder.Language.Substructure.notMem_of_notMem_closure (since := "2025-05-23")]

theorem FirstOrder.Language.Substructure.not_mem_of_not_mem_closure {L : Language} {M : Type w} [L.Structure M] {s : Set M} {P : M} (hP : P ∉ (closure L).toFun s) :

P ∉ s

Alias of FirstOrder.Language.Substructure.notMem_of_notMem_closure.

source

@[simp]

theorem FirstOrder.Language.Substructure.closed {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

(closure L).closed ↑S

source

@[simp]

theorem FirstOrder.Language.Substructure.closure_le {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} :

(closure L).toFun s ≤ S ↔ s ⊆ ↑S

A substructure S includes closure L s if and only if it includes s.

source

theorem FirstOrder.Language.Substructure.closure_mono {L : Language} {M : Type w} [L.Structure M] ⦃s t : Set M⦄ (h : s ⊆ t) :

(closure L).toFun s ≤ (closure L).toFun t

Substructure closure of a set is monotone in its argument: if s ⊆ t, then closure L s ≤ closure L t.

source

theorem FirstOrder.Language.Substructure.closure_eq_of_le {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ (closure L).toFun s) :

(closure L).toFun s = S

source

theorem FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize {L : Language} {M : Type w} [L.Structure M] {s : Set M} :

↑((closure L).toFun s) = Set.range (Term.realize Subtype.val)

source

instance FirstOrder.Language.Substructure.small_closure {L : Language} {M : Type w} [L.Structure M] {s : Set M} [Small.{u, w} ↑s] :

Small.{u, w} ↥((closure L).toFun s)

source

theorem FirstOrder.Language.Substructure.mem_closure_iff_exists_term {L : Language} {M : Type w} [L.Structure M] {s : Set M} {x : M} :

x ∈ (closure L).toFun s ↔ ∃ (t : L.Term ↑s), Term.realize Subtype.val t = x

source

theorem FirstOrder.Language.Substructure.lift_card_closure_le_card_term {L : Language} {M : Type w} [L.Structure M] {s : Set M} :

Cardinal.lift.{max u w, w} (Cardinal.mk ↥((closure L).toFun s)) ≤ Cardinal.mk (L.Term ↑s)

source

theorem FirstOrder.Language.Substructure.lift_card_closure_le {L : Language} {M : Type w} [L.Structure M] {s : Set M} :

Cardinal.lift.{u, w} (Cardinal.mk ↥((closure L).toFun s)) ≤ max Cardinal.aleph0 (Cardinal.lift.{u, w} (Cardinal.mk ↑s) + Cardinal.lift.{w, u} (Cardinal.mk ((i : ℕ) × L.Functions i)))

source

theorem FirstOrder.Language.Substructure.mem_closed_iff {L : Language} {M : Type w} [L.Structure M] (s : Set M) :

s ∈ (closure L).closed ↔ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s

source

theorem FirstOrder.Language.Substructure.mem_closed_of_isRelational (L : Language) {M : Type w} [L.Structure M] [L.IsRelational] (s : Set M) :

s ∈ (closure L).closed

source

@[simp]

theorem FirstOrder.Language.Substructure.closure_eq_of_isRelational (L : Language) {M : Type w} [L.Structure M] [L.IsRelational] (s : Set M) :

↑((closure L).toFun s) = s

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_closure_iff_of_isRelational (L : Language) {M : Type w} [L.Structure M] [L.IsRelational] (s : Set M) (m : M) :

m ∈ (closure L).toFun s ↔ m ∈ s

source

theorem Set.Countable.substructure_closure (L : FirstOrder.Language) {M : Type w} [L.Structure M] {s : Set M} [Countable ((l : ℕ) × L.Functions l)] (h : s.Countable) :

Countable ↥((FirstOrder.Language.Substructure.closure L).toFun s)

source

theorem FirstOrder.Language.Substructure.closure_induction {L : Language} {M : Type w} [L.Structure M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ (closure L).toFun s) (Hs : ∀ x ∈ s, p x) (Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)) :

p x

An induction principle for closure membership. If p holds for all elements of s, and is preserved under function symbols, then p holds for all elements of the closure of s.

source

theorem FirstOrder.Language.Substructure.dense_induction {L : Language} {M : Type w} [L.Structure M] {p : M → Prop} (x : M) {s : Set M} (hs : (closure L).toFun s = ⊤) (Hs : ∀ x ∈ s, p x) (Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)) :

p x

If s is a dense set in a structure M, Substructure.closure L s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p is preserved under function symbols.

source

def FirstOrder.Language.Substructure.gi (L : Language) (M : Type w) [L.Structure M] :

GaloisInsertion (closure L).toFun SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.closure_eq {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

(closure L).toFun ↑S = S

Closure of a substructure S equals S.

source

@[simp]

theorem FirstOrder.Language.Substructure.closure_empty {L : Language} {M : Type w} [L.Structure M] :

(closure L).toFun ∅ = ⊥

source

@[simp]

theorem FirstOrder.Language.Substructure.closure_univ {L : Language} {M : Type w} [L.Structure M] :

(closure L).toFun Set.univ = ⊤

source

theorem FirstOrder.Language.Substructure.closure_union {L : Language} {M : Type w} [L.Structure M] (s t : Set M) :

(closure L).toFun (s ∪ t) = (closure L).toFun s ⊔ (closure L).toFun t

source

theorem FirstOrder.Language.Substructure.closure_iUnion {L : Language} {M : Type w} [L.Structure M] {ι : Sort u_3} (s : ι → Set M) :

(closure L).toFun (⋃ (i : ι), s i) = ⨆ (i : ι), (closure L).toFun (s i)

source

theorem FirstOrder.Language.Substructure.closure_insert {L : Language} {M : Type w} [L.Structure M] (s : Set M) (m : M) :

(closure L).toFun (insert m s) = (closure L).toFun {m} ⊔ (closure L).toFun s

source

instance FirstOrder.Language.Substructure.small_bot {L : Language} {M : Type w} [L.Structure M] :

Small.{u, w} ↥⊥

source

theorem FirstOrder.Language.Substructure.iSup_eq_closure {L : Language} {M : Type w} [L.Structure M] {ι : Sort u_3} (S : ι → L.Substructure M) :

⨆ (i : ι), S i = (closure L).toFun (⋃ (i : ι), ↑(S i))

source

theorem FirstOrder.Language.Substructure.mem_iSup_of_directed {L : Language} {M : Type w} [L.Structure M] {ι : Type u_3} [hι : Nonempty ι] {S : ι → L.Substructure M} (hS : Directed (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) {x : M} :

x ∈ ⨆ (i : ι), S i ↔ ∃ (i : ι), x ∈ S i

source

theorem FirstOrder.Language.Substructure.mem_sSup_of_directedOn {L : Language} {M : Type w} [L.Structure M] {S : Set (L.Substructure M)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) {x : M} :

x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

source

instance FirstOrder.Language.Substructure.instIsEmptySubtypeMemBotOfConstants (L : Language) (M : Type w) [L.Structure M] [IsEmpty L.Constants] :

IsEmpty ↥⊥

`comap` and `map` #

source

def FirstOrder.Language.Substructure.comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure N) :

L.Substructure M

The preimage of a substructure along a homomorphism is a substructure.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure N) :

↑(comap φ S) = ⇑φ ⁻¹' ↑S

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom M N} {x : M} :

x ∈ comap f S ↔ f x ∈ S

source

theorem FirstOrder.Language.Substructure.comap_comap {L : Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.Substructure P) (g : L.Hom N P) (f : L.Hom M N) :

comap f (comap g S) = comap (g.comp f) S

source

@[simp]

theorem FirstOrder.Language.Substructure.comap_id {L : Language} {P : Type u_2} [L.Structure P] (S : L.Substructure P) :

comap (Hom.id L P) S = S

source

def FirstOrder.Language.Substructure.map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure M) :

L.Substructure N

The image of a substructure along a homomorphism is a substructure.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure M) :

↑(map φ S) = ⇑φ '' ↑S

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {S : L.Substructure M} {y : N} :

y ∈ map f S ↔ ∃ x ∈ S, f x = y

source

theorem FirstOrder.Language.Substructure.mem_map_of_mem {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) {S : L.Substructure M} {x : M} (hx : x ∈ S) :

f x ∈ map f S

source

theorem FirstOrder.Language.Substructure.apply_coe_mem_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (S : L.Substructure M) (x : ↥S) :

f ↑x ∈ map f S

source

theorem FirstOrder.Language.Substructure.map_map {L : Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.Substructure M) (g : L.Hom N P) (f : L.Hom M N) :

map g (map f S) = map (g.comp f) S

source

theorem FirstOrder.Language.Substructure.map_le_iff_le_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {S : L.Substructure M} {T : L.Substructure N} :

map f S ≤ T ↔ S ≤ comap f T

source

theorem FirstOrder.Language.Substructure.gc_map_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :

GaloisConnection (map f) (comap f)

source

theorem FirstOrder.Language.Substructure.map_le_of_le_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom M N} :

S ≤ comap f T → map f S ≤ T

source

theorem FirstOrder.Language.Substructure.le_comap_of_map_le {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom M N} :

map f S ≤ T → S ≤ comap f T

source

theorem FirstOrder.Language.Substructure.le_comap_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {f : L.Hom M N} :

S ≤ comap f (map f S)

source

theorem FirstOrder.Language.Substructure.map_comap_le {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom M N} :

map f (comap f S) ≤ S

source

theorem FirstOrder.Language.Substructure.monotone_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} :

Monotone (map f)

source

theorem FirstOrder.Language.Substructure.monotone_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} :

Monotone (comap f)

source

@[simp]

theorem FirstOrder.Language.Substructure.map_comap_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {f : L.Hom M N} :

map f (comap f (map f S)) = map f S

source

@[simp]

theorem FirstOrder.Language.Substructure.comap_map_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom M N} :

comap f (map f (comap f S)) = comap f S

source

theorem FirstOrder.Language.Substructure.map_sup {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S T : L.Substructure M) (f : L.Hom M N) :

map f (S ⊔ T) = map f S ⊔ map f T

source

theorem FirstOrder.Language.Substructure.map_iSup {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Sort u_3} (f : L.Hom M N) (s : ι → L.Substructure M) :

map f (⨆ (i : ι), s i) = ⨆ (i : ι), map f (s i)

source

theorem FirstOrder.Language.Substructure.comap_inf {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S T : L.Substructure N) (f : L.Hom M N) :

comap f (S ⊓ T) = comap f S ⊓ comap f T

source

theorem FirstOrder.Language.Substructure.comap_iInf {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Sort u_3} (f : L.Hom M N) (s : ι → L.Substructure N) :

comap f (⨅ (i : ι), s i) = ⨅ (i : ι), comap f (s i)

source

@[simp]

theorem FirstOrder.Language.Substructure.map_bot {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :

map f ⊥ = ⊥

source

@[simp]

theorem FirstOrder.Language.Substructure.comap_top {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :

comap f ⊤ = ⊤

source

@[simp]

theorem FirstOrder.Language.Substructure.map_id {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

map (Hom.id L M) S = S

source

theorem FirstOrder.Language.Substructure.map_closure {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (s : Set M) :

map f ((closure L).toFun s) = (closure L).toFun (⇑f '' s)

source

@[simp]

theorem FirstOrder.Language.Substructure.closure_image {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {s : Set M} (f : L.Hom M N) :

(closure L).toFun (⇑f '' s) = map f ((closure L).toFun s)

source

def FirstOrder.Language.Substructure.gciMapComap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) :

GaloisCoinsertion (map f) (comap f)

map f and comap f form a GaloisCoinsertion when f is injective.

Equations

Instances For

source

theorem FirstOrder.Language.Substructure.comap_map_eq_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : L.Substructure M) :

comap f (map f S) = S

source

theorem FirstOrder.Language.Substructure.comap_surjective_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) :

Function.Surjective (comap f)

source

theorem FirstOrder.Language.Substructure.map_injective_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) :

Function.Injective (map f)

source

theorem FirstOrder.Language.Substructure.comap_inf_map_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) (S T : L.Substructure M) :

comap f (map f S ⊓ map f T) = S ⊓ T

source

theorem FirstOrder.Language.Substructure.comap_iInf_map_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : ι → L.Substructure M) :

comap f (⨅ (i : ι), map f (S i)) = ⨅ (i : ι), S i

source

theorem FirstOrder.Language.Substructure.comap_sup_map_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) (S T : L.Substructure M) :

comap f (map f S ⊔ map f T) = S ⊔ T

source

theorem FirstOrder.Language.Substructure.comap_iSup_map_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : ι → L.Substructure M) :

comap f (⨆ (i : ι), map f (S i)) = ⨆ (i : ι), S i

source

theorem FirstOrder.Language.Substructure.map_le_map_iff_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) {S T : L.Substructure M} :

map f S ≤ map f T ↔ S ≤ T

source

theorem FirstOrder.Language.Substructure.map_strictMono_of_injective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) :

StrictMono (map f)

source

def FirstOrder.Language.Substructure.giMapComap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) :

GaloisInsertion (map f) (comap f)

map f and comap f form a GaloisInsertion when f is surjective.

Equations

Instances For

source

theorem FirstOrder.Language.Substructure.map_comap_eq_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : L.Substructure N) :

map f (comap f S) = S

source

theorem FirstOrder.Language.Substructure.map_surjective_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) :

Function.Surjective (map f)

source

theorem FirstOrder.Language.Substructure.comap_injective_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) :

Function.Injective (comap f)

source

theorem FirstOrder.Language.Substructure.map_inf_comap_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S T : L.Substructure N) :

map f (comap f S ⊓ comap f T) = S ⊓ T

source

theorem FirstOrder.Language.Substructure.map_iInf_comap_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : ι → L.Substructure N) :

map f (⨅ (i : ι), comap f (S i)) = ⨅ (i : ι), S i

source

theorem FirstOrder.Language.Substructure.map_sup_comap_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S T : L.Substructure N) :

map f (comap f S ⊔ comap f T) = S ⊔ T

source

theorem FirstOrder.Language.Substructure.map_iSup_comap_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : ι → L.Substructure N) :

map f (⨆ (i : ι), comap f (S i)) = ⨆ (i : ι), S i

source

theorem FirstOrder.Language.Substructure.comap_le_comap_iff_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) {S T : L.Substructure N} :

comap f S ≤ comap f T ↔ S ≤ T

source

theorem FirstOrder.Language.Substructure.comap_strictMono_of_surjective {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) :

StrictMono (comap f)

source

instance FirstOrder.Language.Substructure.inducedStructure {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} :

L.Structure ↥S

Equations

source

def FirstOrder.Language.Substructure.subtype {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

L.Embedding (↥S) M

The natural embedding of an L.Substructure of M into M.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.subtype_apply {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {x : ↥S} :

S.subtype x = ↑x

source

theorem FirstOrder.Language.Substructure.subtype_injective {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

Function.Injective ⇑S.subtype

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_subtype {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

⇑S.subtype = Subtype.val

source

@[deprecated FirstOrder.Language.Substructure.coe_subtype (since := "2025-02-18")]

theorem FirstOrder.Language.Substructure.coeSubtype {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

⇑S.subtype = Subtype.val

Alias of FirstOrder.Language.Substructure.coe_subtype.

source

def FirstOrder.Language.Substructure.topEquiv {L : Language} {M : Type w} [L.Structure M] :

L.Equiv (↥⊤) M

The equivalence between the maximal substructure of a structure and the structure itself.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_topEquiv {L : Language} {M : Type w} [L.Structure M] :

⇑topEquiv = Subtype.val

source

@[simp]

theorem FirstOrder.Language.Substructure.realize_boundedFormula_top {L : Language} {M : Type w} [L.Structure M] {α : Type u_3} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → ↥⊤} {xs : Fin n → ↥⊤} :

φ.Realize v xs ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

source

@[simp]

theorem FirstOrder.Language.Substructure.realize_formula_top {L : Language} {M : Type w} [L.Structure M] {α : Type u_3} {φ : L.Formula α} {v : α → ↥⊤} :

φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)

source

theorem FirstOrder.Language.Substructure.closure_induction' {L : Language} {M : Type w} [L.Structure M] (s : Set M) {p : (x : M) → x ∈ (closure L).toFun s → Prop} (Hs : ∀ (x : M) (h : x ∈ s), p x ⋯) (Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x : M | ∃ (hx : x ∈ (closure L).toFun s), p x hx}) {x : M} (hx : x ∈ (closure L).toFun s) :

p x hx

A dependent version of Substructure.closure_induction.

source

def FirstOrder.Language.LHom.substructureReduct {L : Language} {M : Type w} [L.Structure M] {L' : Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] :

L'.Substructure M ↪o L.Substructure M

Reduces the language of a substructure along a language hom.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.LHom.mem_substructureReduct {L : Language} {M : Type w} [L.Structure M] {L' : Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {x : M} {S : L'.Substructure M} :

x ∈ φ.substructureReduct S ↔ x ∈ S

source

@[simp]

theorem FirstOrder.Language.LHom.coe_substructureReduct {L : Language} {M : Type w} [L.Structure M] {L' : Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {S : L'.Substructure M} :

↑(φ.substructureReduct S) = ↑S

source

def FirstOrder.Language.Substructure.withConstants {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) {A : Set M} (h : A ⊆ ↑S) :

(L.withConstants ↑A).Substructure M

Turns any substructure containing a constant set A into a L[[A]]-substructure.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.mem_withConstants {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {A : Set M} (h : A ⊆ ↑S) {x : M} :

x ∈ S.withConstants h ↔ x ∈ S

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_withConstants {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {A : Set M} (h : A ⊆ ↑S) :

↑(S.withConstants h) = ↑S

source

@[simp]

theorem FirstOrder.Language.Substructure.reduct_withConstants {L : Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {A : Set M} (h : A ⊆ ↑S) :

(L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) = S

source

theorem FirstOrder.Language.Substructure.subset_closure_withConstants {L : Language} {M : Type w} [L.Structure M] {A s : Set M} :

A ⊆ ↑((closure (L.withConstants ↑A)).toFun s)

source

theorem FirstOrder.Language.Substructure.closure_withConstants_eq {L : Language} {M : Type w} [L.Structure M] {A s : Set M} :

(closure (L.withConstants ↑A)).toFun s = ((closure L).toFun (A ∪ s)).withConstants ⋯

source

def FirstOrder.Language.Hom.domRestrict {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (p : L.Substructure M) :

L.Hom (↥p) N

The restriction of a first-order hom to a substructure s ⊆ M gives a hom s → N.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Hom.domRestrict_toFun {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (p : L.Substructure M) (a✝ : ↥p) :

(f.domRestrict p) a✝ = f ↑a✝

source

def FirstOrder.Language.Hom.codRestrict {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Hom M N) (h : ∀ (c : M), f c ∈ p) :

L.Hom M ↥p

A first-order hom f : M → N whose values lie in a substructure p ⊆ N can be restricted to a hom M → p.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Hom.codRestrict_toFun_coe {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Hom M N) (h : ∀ (c : M), f c ∈ p) (c : M) :

↑((codRestrict p f h) c) = f c

source

@[simp]

theorem FirstOrder.Language.Hom.comp_codRestrict {L : Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Hom M N) (g : L.Hom N P) (p : L.Substructure P) (h : ∀ (b : N), g b ∈ p) :

(codRestrict p g h).comp f = codRestrict p (g.comp f) ⋯

source

@[simp]

theorem FirstOrder.Language.Hom.subtype_comp_codRestrict {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (p : L.Substructure N) (h : ∀ (b : M), f b ∈ p) :

p.subtype.toHom.comp (codRestrict p f h) = f

source

def FirstOrder.Language.Hom.range {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :

L.Substructure N

The range of a first-order hom f : M → N is a submodule of N. See Note [range copy pattern].

Equations

Instances For

source

theorem FirstOrder.Language.Hom.range_coe {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :

↑f.range = Set.range ⇑f

source

@[simp]

theorem FirstOrder.Language.Hom.mem_range {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {x : N} :

x ∈ f.range ↔ ∃ (y : M), f y = x

source

theorem FirstOrder.Language.Hom.range_eq_map {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :

f.range = Substructure.map f ⊤

source

theorem FirstOrder.Language.Hom.mem_range_self {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (x : M) :

f x ∈ f.range

source

@[simp]

theorem FirstOrder.Language.Hom.range_id {L : Language} {M : Type w} [L.Structure M] :

(id L M).range = ⊤

source

theorem FirstOrder.Language.Hom.range_comp {L : Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Hom M N) (g : L.Hom N P) :

(g.comp f).range = Substructure.map g f.range

source

theorem FirstOrder.Language.Hom.range_comp_le_range {L : Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Hom M N) (g : L.Hom N P) :

(g.comp f).range ≤ g.range

source

theorem FirstOrder.Language.Hom.range_eq_top {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} :

f.range = ⊤ ↔ Function.Surjective ⇑f

source

theorem FirstOrder.Language.Hom.range_le_iff_comap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {p : L.Substructure N} :

f.range ≤ p ↔ Substructure.comap f p = ⊤

source

theorem FirstOrder.Language.Hom.map_le_range {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {p : L.Substructure M} :

Substructure.map f p ≤ f.range

source

def FirstOrder.Language.Hom.eqLocus {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f g : L.Hom M N) :

L.Substructure M

The substructure of elements x : M such that f x = g x

Equations

Instances For

source

theorem FirstOrder.Language.Hom.eqOn_closure {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f g : L.Hom M N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) :

Set.EqOn ⇑f ⇑g ↑((Substructure.closure L).toFun s)

If two L.Homs are equal on a set, then they are equal on its substructure closure.

source

theorem FirstOrder.Language.Hom.eq_of_eqOn_top {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f g : L.Hom M N} (h : Set.EqOn ⇑f ⇑g ↑⊤) :

f = g

source

theorem FirstOrder.Language.Hom.eq_of_eqOn_dense {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {s : Set M} (hs : (Substructure.closure L).toFun s = ⊤) {f g : L.Hom M N} (h : Set.EqOn (⇑f) (⇑g) s) :

f = g

source

def FirstOrder.Language.Embedding.domRestrict {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) :

L.Embedding (↥p) N

The restriction of a first-order embedding to a substructure s ⊆ M gives an embedding s → N.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Embedding.domRestrict_apply {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) (x : ↥p) :

(f.domRestrict p) x = f ↑x

source

def FirstOrder.Language.Embedding.codRestrict {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) (h : ∀ (c : M), f c ∈ p) :

L.Embedding M ↥p

A first-order embedding f : M → N whose values lie in a substructure p ⊆ N can be restricted to an embedding M → p.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Embedding.codRestrict_apply {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c ∈ p} (x : M) :

↑((codRestrict p f h) x) = f x

source

@[simp]

theorem FirstOrder.Language.Embedding.codRestrict_apply' {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c ∈ p} (x : M) :

(codRestrict p f h) x = ⟨f x, ⋯⟩

source

@[simp]

theorem FirstOrder.Language.Embedding.comp_codRestrict {L : Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Embedding M N) (g : L.Embedding N P) (p : L.Substructure P) (h : ∀ (b : N), g b ∈ p) :

(codRestrict p g h).comp f = codRestrict p (g.comp f) ⋯

source

@[simp]

theorem FirstOrder.Language.Embedding.subtype_comp_codRestrict {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure N) (h : ∀ (b : M), f b ∈ p) :

p.subtype.comp (codRestrict p f h) = f

source

noncomputable def FirstOrder.Language.Embedding.substructureEquivMap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (s : L.Substructure M) :

L.Equiv ↥s ↥(Substructure.map f.toHom s)

The equivalence between a substructure s and its image s.map f.toHom, where f is an embedding.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Embedding.substructureEquivMap_apply {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) (x : ↥p) :

↑((f.substructureEquivMap p) x) = f ↑x

source

@[simp]

theorem FirstOrder.Language.Embedding.subtype_substructureEquivMap {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (s : L.Substructure M) :

(Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

source

noncomputable def FirstOrder.Language.Embedding.equivRange {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :

L.Equiv M ↥f.toHom.range

The equivalence between the domain and the range of an embedding f.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Embedding.equivRange_toEquiv_apply {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (a : M) :

f.equivRange.toEquiv a = (codRestrict f.toHom.range f ⋯) a

source

@[simp]

theorem FirstOrder.Language.Embedding.equivRange_apply {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (x : M) :

↑(f.equivRange x) = f x

source

@[simp]

theorem FirstOrder.Language.Embedding.subtype_equivRange {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :

f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

source

theorem FirstOrder.Language.Equiv.toHom_range {L : Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :

f.toHom.range = ⊤

source

def FirstOrder.Language.Substructure.inclusion {L : Language} {M : Type w} [L.Structure M] {S T : L.Substructure M} (h : S ≤ T) :

L.Embedding ↥S ↥T

The embedding associated to an inclusion of substructures.

Equations

Instances For

source

@[simp]

theorem FirstOrder.Language.Substructure.inclusion_self {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

inclusion ⋯ = Embedding.refl L ↥S

source

@[simp]

theorem FirstOrder.Language.Substructure.coe_inclusion {L : Language} {M : Type w} [L.Structure M] {S T : L.Substructure M} (h : S ≤ T) :

⇑(inclusion h) = Set.inclusion h

source

theorem FirstOrder.Language.Substructure.range_subtype {L : Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

S.subtype.toHom.range = S

source

@[simp]

theorem FirstOrder.Language.Substructure.subtype_comp_inclusion {L : Language} {M : Type w} [L.Structure M] {S T : L.Substructure M} (h : S ≤ T) :

T.subtype.comp (inclusion h) = S.subtype

Documentation

Mathlib.ModelTheory.Substructures

First-Order Substructures #

Main Definitions #

Main Results #

`comap` and `map` #

First-Order Substructures #

Main Definitions #

Main Results #

comap and map #

`comap` and `map` #