toNonUnitalSubalgebra_bot — Mathlib

English

The bottom (⊥) subalgebra maps to the bottom NonUnitalSubalgebra.

Русский

Нижняя подалгебра отображается в нижнюю подалгебру без единицы.

LaTeX

$$$(\\,S)^{\\text{toNonUnitalSubalgebra}} = \\bot$$$

Lean4

theorem toNonUnitalSubalgebra_bot : (⊥ : NonUnitalStarSubalgebra R A).toNonUnitalSubalgebra = ⊥ :=
  by
  ext x
  simp only [mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.mem_bot]

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