cg_iff — Mathlib

English

An equivalence expresses that a substructure cg property is preserved under L-structure isomorphism; equivalently, cg is invariant under L-equivalences.

Русский

Эквивалентность показывает, что свойство cg подструктуры сохраняется при изоморфизма структур L; cg инвариантно относительно эквивалентностей L.

LaTeX

$$$$ CG\\;L\\;M \\quad\\text{эквивалентно} \\quad \\exists S,\\; S\\text{ Countable and }\\text{closure}_L(S)=\\top.$$$$

Lean4

/-- An equivalent expression of `Structure.cg`. -/
theorem cg_iff : CG L M ↔ ∃ S : Set M, S.Countable ∧ closure L S = (⊤ : L.Substructure M) := by
  rw [cg_def, Substructure.cg_def]

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