starClosure_le — Mathlib

English

If a subalgebra S1 is contained in a star-subalgebra S2 (when viewed as a subalgebra), then the star-closure of S1 is contained in S2. This captures the minimality of starClosure.

Русский

Если подалгебра S1 лежит внутри подалгебры S2, то звёздное замыкание S1 вложено в S2. Это выражает минимальность starClosure.

LaTeX

$$$S_1^{\star-closure} \le S_2 \quad\Rightarrow\quad S_1 \le S_2^{\,toSubalgebra}$$$

Lean4

theorem starClosure_le {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂.toSubalgebra) :
    S₁.starClosure ≤ S₂ :=
  StarSubalgebra.toSubalgebra_le_iff.1 <|
    sup_le h fun x hx => (star_star x ▸ star_mem (show star x ∈ S₂ from h <| (S₁.mem_star_iff _).1 hx) : x ∈ S₂)

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