fg_iff_exists_fin_generating_family

English

A finitely generated substructure N is precisely the closure of a finite family of elements from M.

Русский

Конечнопородожденная подструктура N есть точная замыкание конечной семьи элементов из M.

LaTeX

$$$N.FG \iff \exists n \; (s : \mathrm{Fin}(n) \to M), closure_L(\mathrm{range}(s)) = N$$$

Lean4

theorem fg_iff_exists_fin_generating_family {N : L.Substructure M} :
    N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), closure L (range s) = N :=
  by
  rw [fg_def]
  constructor
  · rintro ⟨S, Sfin, hS⟩
    obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
    exact ⟨n, f, hS⟩
  · rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

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