sup — Mathlib

English

If N1 and N2 are finitely generated, their join is finitely generated.

Русский

Если N1 и N2 конечнопорождаемы, их объединение (join) тоже конечнопорождаемо.

LaTeX

$$$N_1.FG \to N_2.FG \Rightarrow (N_1 \sqcup N_2).FG$$$

Lean4

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

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