bot_toSubalgebra — Mathlib

English

The underlying Subalgebra of the bottom StarSubalgebra is exactly the bottom Subalgebra: (⊥ : StarSubalgebra R A).toSubalgebra = ⊥.

Русский

Подложенная подалгебра нижнего элемента отображается в нижнюю подалгебру: (⊥ : StarSubalgebra R A).toSubalgebra = ⊥.

LaTeX

$$$ (\\bot : StarSubalgebra\\; R\\; A).toSubalgebra = \\bot $$$

Lean4

theorem bot_toSubalgebra : (⊥ : StarSubalgebra R A).toSubalgebra = ⊥ :=
  rfl

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