of_finite — Mathlib

English

A substructure N is countably generated iff there exists a countable set S with closure S = N.

Русский

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

LaTeX

$$$N.CG \iff \exists S : Set M, S.Countable \land closure L S = N$$$

Lean4

theorem of_finite {s : L.Substructure M} [h : Finite s] : s.FG :=
  ⟨Set.Finite.toFinset h, by simp only [Finite.coe_toFinset, closure_eq]⟩

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