star_adjoin_comm — Mathlib

English

The star operation on NonUnitalSubalgebra is monotone: if S1 ≤ S2 then star(S1) ≤ star(S2).

Русский

Операция star на NonUnitalSubalgebra монотонна: если S1 ≤ S2, то star(S1) ≤ star(S2).

LaTeX

$$$ S_1 \le S_2 \Rightarrow \mathrm{star}(S_1) \le \mathrm{star}(S_2) $$$

Lean4

/-- The star operation on `NonUnitalSubalgebra` commutes with `NonUnitalAlgebra.adjoin`. -/
theorem star_adjoin_comm (s : Set A) : star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s) :=
  have this : ∀ t : Set A, NonUnitalAlgebra.adjoin R (star t) ≤ star (NonUnitalAlgebra.adjoin R t) := fun _ =>
    NonUnitalAlgebra.adjoin_le fun _ hx => NonUnitalAlgebra.subset_adjoin R hx
  le_antisymm (by simpa only [star_star] using NonUnitalSubalgebra.star_mono (this (star s))) (this s)

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