toNonUnitalSubalgebra_le_iff — Mathlib

English

Order comparison between NonUnitalStarSubalgebra via their nonunital subalgebras is equivalent to the original order.

Русский

Порядковое сравнение через toNonUnitalSubalgebra эквивалентно исходному порядку.

LaTeX

$$$S_1.toNonUnitalSubalgebra \\le S_2.toNonUnitalSubalgebra \\iff S_1 \\le S_2$$$

Lean4

theorem toNonUnitalSubalgebra_le_iff {S₁ S₂ : NonUnitalStarSubalgebra R A} :
    S₁.toNonUnitalSubalgebra ≤ S₂.toNonUnitalSubalgebra ↔ S₁ ≤ S₂ :=
  Iff.rfl

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