sup — Mathlib

English

If two submodules N1 and N2 are finitely generated, then their join N1 ⊔ N2 is finitely generated.

Русский

Если два подмодуля FG, то их сумма (объединение) FG.

LaTeX

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

Lean4

theorem sup {N₁ N₂ : Submodule R 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 [span_union, ht₁.2, ht₂.2]⟩

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