cg_iff_countable — Mathlib

English

If the language has countably many function symbols in the index, then the CG property in M is equivalent to M being countable.

Русский

При счётном числе функциональных символов cg-существо эквивалентно счётности множества элементов.

LaTeX

$$$$ [Countable (\\Sigma l, L.Functions l)] \\Rightarrow (CG\\ L\\ M \\iff\\ Countable\\; M).$$$$

Lean4

theorem cg_iff_countable [Countable (Σ l, L.Functions l)] : CG L M ↔ Countable M := by
  rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]

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