comap_top

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarAlgebra.comap_top

← MathLib Explorer

English

Maps preserve the bottom: the image of the bottom subalgebra is bottom.

Русский

Образ нижней подалгебры под отображением равен нижней подалгебре.

LaTeX

$$$(\\bot : NonUnitalStarSubalgebra R A).map f = \\bot$$$

Lean4

@[simp]
theorem comap_top [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) :
    (⊤ : NonUnitalStarSubalgebra R B).comap f = ⊤ :=
  eq_top_iff.2 fun _x => mem_top

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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