toSubalgebra_inj

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarSubalgebra.toSubalgebra_inj

English

For StarSubalgebras S and U, S.toSubalgebra = U.toSubalgebra if and only if S = U.

Русский

Для звездных подалгебр S и U выполняется: S.toSubalgebra = U.toSubalgebra тогда и только тогда, когда S = U.

LaTeX

$$$S^{\to Subalgebra} = U^{\to Subalgebra} \;\iff\; S = U$$$

Lean4

theorem toSubalgebra_inj {S U : StarSubalgebra R A} : S.toSubalgebra = U.toSubalgebra ↔ S = U :=
  toSubalgebra_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru