starClosure_le_iff — Mathlib

English

For S1 a subalgebra and S2 a star-subalgebra, S1.starClosure ≤ S2 if and only if S1 ≤ S2.toSubalgebra. This provides a convenient criterion for comparing closures with subalgebras.

Русский

Для подалгебры S1 и звёздной подалгебры S2 верна эквивалентность: S1.starClosure ≤ S2 тогда и только тогда, когда S1 ≤ S2.toSubalgebra.

LaTeX

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

Lean4

theorem starClosure_le_iff {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} :
    S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toSubalgebra :=
  ⟨fun h => le_sup_left.trans h, starClosure_le⟩

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