sup — Mathlib

English

If S and S' are finitely generated subalgebras, then their supremum S ⊔ S' is FG.

Русский

Если S и S' — FG-подалгебры, то верхняя граница S ⊔ S' FG.

LaTeX

$$$S.FG \\rightarrow S'.FG \\rightarrow (S \\;\\sqcup\\; S').FG$$$

Lean4

theorem sup {S S' : Subalgebra R A} (hS : Subalgebra.FG S) (hS' : Subalgebra.FG S') : Subalgebra.FG (S ⊔ S') :=
  let ⟨s, hs⟩ := Subalgebra.fg_def.1 hS
  let ⟨s', hs'⟩ := Subalgebra.fg_def.1 hS'
  fg_def.mpr ⟨s ∪ s', Set.Finite.union hs.1 hs'.1, (by rw [Algebra.adjoin_union, hs.2, hs'.2])⟩

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