starClosure — Mathlib

English

The star operation commutes with the adjoin operation: star(adjoin R s) = adjoin R (star s).

Русский

Операция star commuting: star(adjoin R s) = adjoin R (star s).

LaTeX

$$$ \star(\mathrm{adjoin}_R(S)) = \mathrm{adjoin}_R(\star S) $$$

Lean4

/-- The `NonUnitalStarSubalgebra` obtained from `S : NonUnitalSubalgebra R A` by taking the
smallest non-unital subalgebra containing both `S` and `star S`. -/
def starClosure (S : NonUnitalSubalgebra R A) : NonUnitalStarSubalgebra R A
    where
  toNonUnitalSubalgebra := S ⊔ star S
  star_mem' {a}
    ha := by
    simpa [← mem_star_iff _ a, ← (@NonUnitalAlgebra.gi R A _ _ _ _ _).l_sup_u _ _, star_adjoin_comm,
      Set.union_comm] using ha

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