toNonUnitalSubalgebra_inj — Mathlib

English

A lemma stating that two nonunital star subalgebras are equal iff their images under toNonUnitalSubalgebra are equal.

Русский

Лемма: два неполных звёздных подалгебра равны тогда и только тогда, когда их изображения равны.

LaTeX

$$$S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra \\iff S = U$$$

Lean4

theorem toNonUnitalSubalgebra_inj {S U : NonUnitalStarSubalgebra R A} :
    S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U :=
  toNonUnitalSubalgebra_injective.eq_iff

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