sup — Mathlib

English

Another formulation of CG: N.CG iff there exists a countable generating set S such that closure equals N.

Русский

Еще одно формулирование CG: N.CG эквивалентно существованию счётного порождающего множества S, такого что closure S = N.

LaTeX

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

Lean4

theorem sup {N₁ N₂ : L.Substructure M} (hN₁ : N₁.CG) (hN₂ : N₂.CG) : (N₁ ⊔ N₂).CG :=
  let ⟨t₁, ht₁⟩ := cg_def.1 hN₁
  let ⟨t₂, ht₂⟩ := cg_def.1 hN₂
  cg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [closure_union, ht₁.2, ht₂.2]⟩

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