fg_iff — Mathlib

English

FG L M is equivalent to the existence of a finite set S in M whose L-closure is the whole structure.

Русский

Существование множества S = конечного размера в M такое, что замыкание по L даёт всю структуру.

LaTeX

$$$\text{FG}(L,M) \iff \exists S \subseteq M:\, S \text{ finite} \land \operatorname{closure}_L(S) = \top_{L,M}$$$

Lean4

/-- An equivalent expression of `Structure.FG` in terms of `Set.Finite` instead of `Finset`. -/
theorem fg_iff : FG L M ↔ ∃ S : Set M, S.Finite ∧ closure L S = (⊤ : L.Substructure M) := by
  rw [fg_def, Substructure.fg_def]

Похожие утверждения