fg_def — Mathlib

English

A substructure N is finitely generated if and only if there exists a finite set S with closure_S = N.

Русский

Подструктура N конечна порождена тогда и только тогда, когда существует конечный набор S, такой что замыкание S равно N.

LaTeX

$$$N.FG \iff \exists S \subseteq M, S.Finite \wedge closure_L(S) = N$$$

Lean4

theorem fg_def {N : L.Substructure M} : N.FG ↔ ∃ S : Set M, S.Finite ∧ closure L S = N :=
  ⟨fun ⟨t, h⟩ => ⟨_, Finset.finite_toSet t, h⟩, by
    rintro ⟨t', h, rfl⟩
    rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
    exact ⟨t, rfl⟩⟩

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