English
A substructure N is CG if and only if N is empty or N is the closure of a countable range of a sequence of elements from M.
Русский
Подструктура N CG тогда и только тогда, когда она пустая или является замыканием счётной образующей последовательности элементов из M.
LaTeX
$$$N.CG \iff N = \emptyset \lor \exists s : \mathbb{N} \to M, closure L (range s) = N$$$
Lean4
theorem cg_iff_empty_or_exists_nat_generating_family {N : L.Substructure M} :
N.CG ↔ N = (∅ : Set M) ∨ ∃ s : ℕ → M, closure L (range s) = N :=
by
rw [cg_def]
constructor
· rintro ⟨S, Scount, hS⟩
rcases eq_empty_or_nonempty (N : Set M) with h | h
· exact Or.intro_left _ h
obtain ⟨f, h'⟩ := (Scount.union (Set.countable_singleton h.some)).exists_eq_range (singleton_nonempty h.some).inr
refine Or.intro_right _ ⟨f, ?_⟩
rw [← h', closure_union, hS, sup_eq_left, closure_le]
exact singleton_subset_iff.2 h.some_mem
· intro h
rcases h with h | h
· refine ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) ?_⟩
rw [← SetLike.coe_subset_coe, h]
exact empty_subset _
· obtain ⟨f, rfl⟩ := h
exact ⟨range f, countable_range _, rfl⟩
