FirstOrder.Language.Substructure.ext
theorem FirstOrder.Language.Substructure.ext :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S T : L.Substructure M},
(∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any given first-order language `L` and any type `M` that is a structure for `L`, two substructures `S` and `T` of `L` over `M` are equal if they contain the same elements. In other words, if every element `x` of type `M` is in `S` if and only if it is in `T`, then `S` and `T` are the same substructure.
More concisely: If two substructures of a first-order structure over a base type have the same elements, then they are equal.
|
Mathlib.ModelTheory.Substructures._auxLemma.23
theorem Mathlib.ModelTheory.Substructures._auxLemma.23 :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
{f : L.Hom M N} {x : N}, (x ∈ f.range) = ∃ y, f y = x
This theorem asserts that for any first-order language `L`, types `M` and `N`, and given the structures of `L` on `M` and `N`, if `f` is a homomorphism from `M` to `N` and `x` is an element of `N`, then `x` is in the range of `f` if and only if there exists an element `y` in `M` such that `f(y)` equals `x`. In other words, an element `x` of `N` belongs to the range of the homomorphism `f` iff `x` is the image of some element in `M` under `f`.
More concisely: For any homomorphism $f$ from type $M$ to type $N$ in a first-order language $L$, and for any $x$ in $N$, $x$ is in the image of $f$ if and only if there exists an $y$ in $M$ such that $f(y) = x$.
|
FirstOrder.Language.Hom.eqOn_closure
theorem FirstOrder.Language.Hom.eqOn_closure :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
{f g : L.Hom M N} {s : Set M},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑((FirstOrder.Language.Substructure.closure L).toFun s)
The theorem `FirstOrder.Language.Hom.eqOn_closure` states that in the context of a first-order language `L`, and two structures `M` and `N` over this language, if two homomorphisms `f` and `g` from `M` to `N` are equal on a set `s` (meaning that for every element in `s`, `f` and `g` give the same result), then `f` and `g` are also equal on the substructure closure of `s`. In essence, the equality of two homomorphisms on a set extends to the equality on its substructure closure in the language.
More concisely: If homomorphisms $f$ and $g$ from structure $M$ to $N$ in a first-order language agree on a set $s$, then they agree on the substructure closure of $s$ in $M$.
|
FirstOrder.Language.Substructure.closure_mono
theorem FirstOrder.Language.Substructure.closure_mono :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] ⦃s t : Set M⦄,
s ⊆ t →
(FirstOrder.Language.Substructure.closure L).toFun s ≤ (FirstOrder.Language.Substructure.closure L).toFun t
This theorem states that the substructure closure of a set is monotone with respect to its input set. In particular, given a first order language `L` and a type `M` that has a `L.Structure` instance, if we have two sets `s` and `t` of type `M` such that `s` is a subset of `t`, then the substructure closure of `s` (under the language `L`) is less than or equal to the substructure closure of `t` (under the same language `L`). In other words, increasing your input set to the substructure closure operation cannot decrease the size of the closure.
More concisely: If `L` is a first order language and `M` has an `L.Structure` instance, then for any sets `s` and `t` of type `M` with `s` a subset of `t`, the substructure closure of `s` under `L` is included in the substructure closure of `t` under `L`.
|
FirstOrder.Language.Hom.range_eq_map
theorem FirstOrder.Language.Hom.range_eq_map :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
(f : L.Hom M N), f.range = FirstOrder.Language.Substructure.map f ⊤
This theorem states that for any first-order language `L`, and any types `M` and `N` with structures of `L`, the range of a homomorphism `f : M → N` is equivalent to the image of the entire structure `M` (denoted by the top element `⊤`) under the homomorphism `f`. In other words, applying `f` to all elements of `M` gives us the same set as the range of `f`.
More concisely: For any first-order language L, any types M and N with structures, and any homomorphism f : M -> N, the range of f is equal to the image of the entire structure M under f (denoted by f(⊤)).
|
Mathlib.ModelTheory.Substructures._auxLemma.3
theorem Mathlib.ModelTheory.Substructures._auxLemma.3 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (x : M), (x ∈ ⊤) = True
This theorem states that for any first-order language `L` and any type `M` that has a structure for `L`, every element `x` of type `M` will always belong to the top element (`⊤`) of the lattice of substructures of `M`. In other words, `x` is always part of the whole structure `M` under any interpretation in the language `L`. This is a fundamental fact from the model theory, a branch of mathematical logic that deals with the relationship between a formal language and its interpretations.
More concisely: For any first-order language L and any type M with an L-structure, every element x of M belongs to the top element (⊤) of the lattice of substructures of M.
|
FirstOrder.Language.Substructure.closure_induction'
theorem FirstOrder.Language.Substructure.closure_induction' :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s : Set M)
{p : (x : M) → x ∈ (FirstOrder.Language.Substructure.closure L).toFun s → Prop},
(∀ (x : M) (h : x ∈ s), p x ⋯) →
(∀ {n : ℕ} (f : L.Functions n),
FirstOrder.Language.ClosedUnder f
{x | ∃ (hx : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s), p x hx}) →
∀ {x : M} (hx : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s), p x hx
This theorem, `FirstOrder.Language.Substructure.closure_induction'`, establishes a principle of induction for a dependent predicate over elements in the closure of a set under a structure in a first-order language. Specifically, it states that if a predicate `p` holds for all elements in a set `s`, and if `p` holds for elements resulting from the application of any function symbol of the language on elements in the closure of `s` where `p` holds, then `p` holds for all elements in the closure of `s`. In other words, we can inductively establish the property `p` for all elements in the closure if `p` holds for elements in the initial set and remains true under the operations of the language.
More concisely: If a predicate holds for all elements in a set and closures of elements under function symbols where the predicate holds, then the predicate holds for all elements in the closure of the set.
|
Mathlib.ModelTheory.Substructures._auxLemma.13
theorem Mathlib.ModelTheory.Substructures._auxLemma.13 :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
{S : L.Substructure N} {f : L.Hom M N} {x : M}, (x ∈ FirstOrder.Language.Substructure.comap f S) = (f x ∈ S)
This theorem states that for any first-order language `L`, any types `M` and `N`, any structures `inst` of `L` over `M` and `inst_1` of `L` over `N`, any substructure `S` of `L` over `N`, any homomorphism `f` from `M` to `N`, and any element `x` of `M`, the element `x` is in the preimage of the substructure `S` under the homomorphism `f` if and only if the image of `x` under `f` is in `S`. This is a fundamental property of preimages under homomorphisms in the context of substructures in model theory.
More concisely: For any homomorphism between structures and any substructure, an element is in the preimage of the substructure if and only if its image is in the substructure.
|
FirstOrder.Language.Substructure.closure_eq_of_le
theorem FirstOrder.Language.Substructure.closure_eq_of_le :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M},
s ⊆ ↑S →
S ≤ (FirstOrder.Language.Substructure.closure L).toFun s →
(FirstOrder.Language.Substructure.closure L).toFun s = S
This theorem states that for any first-order language `L` and any type `M` with a structure for `L`, given a substructure `S` of `L` on `M`, and a set `s` of elements of `M`, if `s` is a subset of `S` and `S` is less than or equal to the substructure generated by `s`, then the substructure generated by `s` is exactly `S`. In other words, the closure operation that generates the smallest substructure containing a given set is idempotent and preserves order: if `s` is already closed (i.e., is a substructure), the closure operation doesn't change `s`, and if `s` is a proper subset of a substructure `S`, the closure operation can't "jump over" `S` to produce a larger substructure.
More concisely: If `S` is a substructure of `M` in a first-order language `L`, and `s` is a subset of `M` that is closed under `S`, then `s` equals `S`.
|
FirstOrder.Language.Substructure.closure_induction
theorem FirstOrder.Language.Substructure.closure_induction :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} {p : M → Prop} {x : M},
x ∈ (FirstOrder.Language.Substructure.closure L).toFun s →
(∀ x ∈ s, p x) → (∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (setOf p)) → p x
This theorem, named `FirstOrder.Language.Substructure.closure_induction`, represents an induction principle for membership in the closure of a set in a given structure of First Order Logic. Specifically, it states that for any language `L`, structure `M`, set `s` in `M` and a predicate `p` over elements of `M`, if a particular element `x` belongs to the closure of `s` under `L`, and if the predicate `p` holds for all elements of `s` as well as being preserved under function symbols of `L`, then `p` also holds for `x`. In other words, if `p` is true for all elements of `s` and remains true when applying any function from the language to elements of `s`, then `p` is true for every element in the closure of `s`.
More concisely: If a set `s` in a First Order Logic structure `M` and predicate `p` hold for all elements of `s` and are preserved under function symbols of the language `L`, then `p` holds for every element in the closure of `s`.
|
FirstOrder.Language.Substructure.closure_union
theorem FirstOrder.Language.Substructure.closure_union :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s t : Set M),
(FirstOrder.Language.Substructure.closure L).toFun (s ∪ t) =
(FirstOrder.Language.Substructure.closure L).toFun s ⊔ (FirstOrder.Language.Substructure.closure L).toFun t
The theorem `FirstOrder.Language.Substructure.closure_union` states that for any first-order language `L` and any type `M` with a `FirstOrder.Language.Structure` instance, and any two sets `s` and `t` of type `M`, the closure of the union of `s` and `t` in the language `L` is equivalent to the supremum (join operation in the lattice theory) of the closures of `s` and `t` separately in the language `L`. This theorem is essentially expressing that the closure operation respects set unions in the context of first order languages.
More concisely: For any first-order language L and type M with a FirstOrder.Language.Structure instance, the closure of the union of two sets s and t in language L is equal to the join (supremum) of the closures of s and t.
|
FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize
theorem FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M},
↑((FirstOrder.Language.Substructure.closure L).toFun s) =
Set.range (FirstOrder.Language.Term.realize Subtype.val)
This theorem states that for any first-order language `L` and any type `M` with a `FirstOrder.Language.Structure` instance, the substructure generated by a set `s` of `M` (i.e., `(FirstOrder.Language.Substructure.closure L).toFun s`) is equal to the range of the function that realizes a term of `L` in `M` (i.e., `FirstOrder.Language.Term.realize Subtype.val`). In other words, if you generate a substructure by closing a set under the operations of a first-order language, you obtain the same set of elements as if you apply every term of the language to every element of your set.
More concisely: For any first-order language L and type M with a structure instance, the substructure generated by a set s of M equals the range of the function realizing every term of L applied to s.
|
FirstOrder.Language.Substructure.dense_induction
theorem FirstOrder.Language.Substructure.dense_induction :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {p : M → Prop} (x : M) {s : Set M},
(FirstOrder.Language.Substructure.closure L).toFun s = ⊤ →
(∀ x ∈ s, p x) → (∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (setOf p)) → p x
The theorem `FirstOrder.Language.Substructure.dense_induction` states that for any First Order language `L` and a structure `M` of that language, given a predicate `p` on `M` and an arbitrary element `x` in `M`, if a set `s` of `M` is dense in the structure (i.e., `Substructure.closure L s = ⊤`), then to prove that `p` holds for all `x` in `M`, it is sufficient to ensure two conditions: first, `p x` should hold for all `x` in the dense set `s`; second, the predicate `p` must be preserved under all function symbols of the language. In other words, if `p` holds for all elements produced by the function given the arguments from the set `s`, then `p` holds for all `x` in `M`. This theorem is a form of induction principle for densely-defined predicates in algebraic structures.
More concisely: Given a First Order language L and a dense subset s of a structure M in L, if a predicate p holds for all elements in s and is preserved under all function symbols of L, then p holds for all elements in M.
|
FirstOrder.Language.Substructure.map_le_iff_le_comap
theorem FirstOrder.Language.Substructure.map_le_iff_le_comap :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
{f : L.Hom M N} {S : L.Substructure M} {T : L.Substructure N},
FirstOrder.Language.Substructure.map f S ≤ T ↔ S ≤ FirstOrder.Language.Substructure.comap f T
The theorem `FirstOrder.Language.Substructure.map_le_iff_le_comap` states that for any first-order languages `L`, structures `M` and `N`, a homomorphism `f` from `M` to `N`, and substructures `S` of `M` and `T` of `N`, the image of `S` under `f` is a substructure of `T` if and only if `S` is a substructure of the preimage of `T` under `f`. In other words, it establishes a correspondence between the substructures in the domain that map into a given substructure in the codomain, and the substructures in the codomain that are mapped into by a given substructure in the domain, via a given homomorphism.
More concisely: For first-order languages L, structures M and N, a homomorphism f from M to N, and substructures S of M and T of N, S is a substructure of T if and only if the image of S under f is a substructure of T.
|
FirstOrder.Language.Hom.mem_range_self
theorem FirstOrder.Language.Hom.mem_range_self :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
(f : L.Hom M N) (x : M), f x ∈ f.range
This theorem states that for any first-order language `L`, and any two types `M` and `N` that have a `FirstOrder.Language.Structure` over `L`, for any homomorphism `f` from `M` to `N` and any element `x` in `M`, the result of applying `f` to `x` is in the range of `f`. In other words, if you have a function `f` that maps elements of `M` to `N`, every output of `f` is indeed in the set of all possible outputs of `f`.
More concisely: For any first-order language L, any homomorphism f between types M and N with structures over L, and any x in M, we have f(x) ∈ range(f).
|
FirstOrder.Language.Substructure.gc_map_comap
theorem FirstOrder.Language.Substructure.gc_map_comap :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
(f : L.Hom M N),
GaloisConnection (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)
The theorem `FirstOrder.Language.Substructure.gc_map_comap` states that for any first-order language `L`, and any types `M` and `N` that have a `FirstOrder.Language.Structure` over `L`, and for any homomorphism `f` from `M` to `N` in the language `L`, there is a Galois connection between the operation of mapping substructures along `f` and the operation of taking preimages of substructures along `f`. In other words, for a given substructure `S` of `M` and a substructure `T` of `N`, the image of `S` under `f` is a subset of `T` if and only if `S` is a subset of the preimage of `T` under `f`. This is a fundamental property connecting the map and comap operations in the theory of first-order language structures.
More concisely: For any first-order language L, types M and N with structures over L, and homomorphism f from M to N, the mapping of substructures along f and the taking of preimages of substructures along f form a Galois connection.
|
FirstOrder.Language.Substructure.subset_closure
theorem FirstOrder.Language.Substructure.subset_closure :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M},
s ⊆ ↑((FirstOrder.Language.Substructure.closure L).toFun s)
This theorem states that for any first-order language `L`, a type `M`, and a set `s` of elements of type `M`, the substructure generated by `s` in the language `L` contains `s` itself. In other words, every element of the set `s` is also an element of the substructure generated by `s`. This is usually the case in algebraic structures where the substructure generated by a set is the smallest substructure containing that set.
More concisely: For any first-order language L and set s of elements from a type M, the substructure of M generated by s includes s itself.
|
FirstOrder.Language.Substructure.closure_eq
theorem FirstOrder.Language.Substructure.closure_eq :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M),
(FirstOrder.Language.Substructure.closure L).toFun ↑S = S
This theorem states that for any first-order language 'L' and any type 'M' that is a structure for 'L', the closure of a substructure 'S' of 'M' is equal to 'S' itself. In other words, when we generate the `FirstOrder.Language.Substructure` from a set 'S' using the `closure` function, the result is 'S'. This indicates that 'S' is a closed substructure, i.e., it contains all elements that are required by the properties of the first-order language 'L'.
More concisely: For any first-order language L and its structure M, the closure of a substructure S of M equals S itself.
|
FirstOrder.Language.Substructure.closure_le
theorem FirstOrder.Language.Substructure.closure_le :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M},
(FirstOrder.Language.Substructure.closure L).toFun s ≤ S ↔ s ⊆ ↑S
This theorem, `FirstOrder.Language.Substructure.closure_le`, states that for any first-order language `L`, any model `M` of `L`, any substructure `S` of `M`, and any set `s` of elements in `M`, the substructure `S` includes the substructure generated by `s` (denoted as `(FirstOrder.Language.Substructure.closure L).toFun s`) if and only if the substructure `S` includes `s` itself (denoted as `s ⊆ ↑S`). In other words, the closure of a set `s` within a first-order language structure is a subset of a given substructure if and only if the set `s` itself is a subset of that substructure.
More concisely: In a first-order language, a substructure includes the closure of a set if and only if it includes the set itself.
|