toNonUnitalSubalgebra_eq_top — Mathlib

English

For any S, S.toNonUnitalSubalgebra = ⊤ if and only if S = ⊤.

Русский

Для любой S выполняется равенство S.toNonUnitalSubalgebra = ⊤ тогда и только тогда, когда S = ⊤.

LaTeX

$$$$ S.toNonUnitalSubalgebra = \\top \\\\iff S = \\top $$$$

Lean4

@[simp]
theorem toNonUnitalSubalgebra_eq_top {S : NonUnitalStarSubalgebra R A} : S.toNonUnitalSubalgebra = ⊤ ↔ S = ⊤ :=
  NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective.eq_iff' top_toNonUnitalSubalgebra

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