FirstOrder.Language.Structure.cg_iff
theorem FirstOrder.Language.Structure.cg_iff :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M],
FirstOrder.Language.Structure.CG L M ↔
∃ S, S.Countable ∧ (FirstOrder.Language.Substructure.closure L).toFun S = ⊤
This theorem, `FirstOrder.Language.Structure.cg_iff`, provides an alternative characterization for the `Structure.cg` property in the FirstOrder.Language in Lean 4. It states that for any given language `L` of first-order logic and any type `M` that has a `L.Structure` instance, the `Structure.cg` (countable-generated) property holds if and only if there exists a countable substructure `S` such that when the closure operation of `L` is applied to `S`, it yields the top element (⊤), which represents the entire structure. In other words, we can generate the whole structure by taking closures of countable subsets.
More concisely: A first-order language `L`'s `Structure.cg` property holds if and only if there exists a countable substructure `S` such that the closure of `S` under `L`'s operations equals the universe.
|
FirstOrder.Language.Structure.fg_def
theorem FirstOrder.Language.Structure.fg_def :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], FirstOrder.Language.Structure.FG L M ↔ ⊤.FG := by
sorry
This theorem states that for any first-order language `L` and any type `M` with a given `FirstOrder.Language.Structure L M`, the structure `L M` is finitely generated if and only if the maximal substructure, represented by `⊤`, is finitely generated. In mathematical terms, we say a structure is finitely generated if it can be produced by taking a finite set and repeatedly applying the operations of the language to elements of this set.
More concisely: For any first-order language `L` and type `M` in Lean 4 with `FirstOrder.Language.Structure L M`, the structure `L M` is finitely generated if and only if its maximal substructure is finitely generated.
|
FirstOrder.Language.Structure.fg_iff
theorem FirstOrder.Language.Structure.fg_iff :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M],
FirstOrder.Language.Structure.FG L M ↔ ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = ⊤
The theorem `FirstOrder.Language.Structure.fg_iff` is stating that for any first-order language `L` and any model `M` of type `u_1` for `L`, a structure `L.Structure M` is finitely generated (`FirstOrder.Language.Structure.FG L M`) if and only if there exists a set `S` that is finite (`S.Finite`) and the closure of `S` (under the substructure operation defined for `L`) generates the entire structure (`FirstOrder.Language.Substructure.closure L).toFun S = ⊤`).
More concisely: A first-order language's structure over a model is finitely generated if and only if there exists a finite set whose closure under substructures generates the entire structure.
|
FirstOrder.Language.Substructure.FG.cg
theorem FirstOrder.Language.Substructure.FG.cg :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M}, N.FG → N.CG
The theorem `FirstOrder.Language.Substructure.FG.cg` states that for any first-order language `L` and a type `M` that is a structure of `L`, if a substructure `N` of `M` is finitely generated (i.e., it is the closure of a finite subset of `M`), then `N` is also countably generated (i.e., it is the closure of a countable subset of `M`). This is a universal property that holds for all such `L`, `M`, and `N`.
More concisely: If `L` is a first-order language, `M` is an `L`-structure, and `N` is a finitely generated substructure of `M`, then `N` is countably generated.
|
FirstOrder.Language.Substructure.fg_def
theorem FirstOrder.Language.Substructure.fg_def :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M},
N.FG ↔ ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N
This theorem states that for any first-order language `L`, any type `M`, and any `N` which is a substructure of `L` over `M`, `N` is finitely generated if and only if there exists a set `S` which is finite and the substructure generated by `S` is equal to `N`. The substructure generated by `S` means the smallest substructure that contains `S`. This gives a precise mathematical condition for a substructure to be finitely generated in the context of first-order languages.
More concisely: A substructure of a first-order language with respect to a type is finitely generated if and only if there exists a finite set generating it.
|
FirstOrder.Language.Substructure.cg_def
theorem FirstOrder.Language.Substructure.cg_def :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M},
N.CG ↔ ∃ S, S.Countable ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N
This theorem is stating that for any first order language `L` and any type `M` with a structure for `L`, a substructure `N` of `L` on `M` is countably generated if and only if there exists a set `S` such that `S` is countable and the closure of `S` under the substructure operations of `L` equals `N`. Here, a set is countable if there exists an injective function mapping the set to the natural numbers, and the closure of a set under the substructure operations is the smallest substructure that includes the set.
More concisely: A substructure of a first-order language's structure on a type is countably generated if and only if there exists a countable set whose closure under the substructure operations equals the substructure.
|
FirstOrder.Language.Structure.cg_def
theorem FirstOrder.Language.Structure.cg_def :
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], FirstOrder.Language.Structure.CG L M ↔ ⊤.CG := by
sorry
This theorem states that for any first-order language `L` and any type `M` which has a `FirstOrder.Language.Structure` instance, a structure of language `L` on `M` is countably generated if and only if the top-level substructure (`⊤`) of the same language on `M` is countably generated. In other words, a structure is countably generated (i.e., it can be built from a countable set) if the most encompassing substructure can also be constructed from a countable set.
More concisely: For any first-order language L and type M with a Structure instance, the structure of language L on M is countably generated if and only if the top-level substructure of L on M is countably generated.
|