withTop_id

Mathlib.Order.Hom.WithTopBot

URI: https://scilib.ai/kg/mathlib#LatticeHom.withTop_id

English

The top-extended identity is the identity on WithTop.

Русский

Тождественный отображение, расширенное вверх, остаётся тождественным на WithTop.

LaTeX

$$$ (\mathrm{LatticeHom.id}\ \alpha).{\mathrm{withTop}} = \mathrm{LatticeHom.id}\ (\mathrm{WithTop}\ \alpha) $$$

Lean4

@[simp]
theorem withTop_id : (LatticeHom.id α).withTop = LatticeHom.id _ :=
  DFunLike.coe_injective WithTop.map_id

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

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

Разделы

Аффилиация

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