starClosure_eq_adjoin — Mathlib

English

The collection of NonUnitalStarSubalgebra R A forms a complete lattice.

Русский

Множество NonUnitalStarSubalgebra R A образует полностью упорядблюющееся решетку.

LaTeX

$$$$ \\text{CompleteLattice}(\\\\operatorname{NonUnitalStarSubalgebra}\\\\, R, A) $$$$

Lean4

theorem _root_.NonUnitalSubalgebra.starClosure_eq_adjoin (S : NonUnitalSubalgebra R A) :
    S.starClosure = adjoin R (S : Set A) :=
  le_antisymm (NonUnitalSubalgebra.starClosure_le_iff.2 <| subset_adjoin R (S : Set A))
    (adjoin_le (le_sup_left : S ≤ S ⊔ star S))

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