dual_id

Mathlib.Order.Hom.Bounded

URI: https://scilib.ai/kg/mathlib#TopHom.dual_id

English

The dual of the identity top-homomorphism is the bottom identity in the dual setting.

Русский

Двойственность тождественного топ-гомоморфизма даёт тождество в дуальном порядке.

LaTeX

$$$\mathrm{TopHom}.dual(\mathrm{id}_\alpha) = \mathrm{BotHom}.id_{(\mathrm{OrderDual}\alpha)}$$$

Lean4

@[simp]
theorem dual_id : TopHom.dual (TopHom.id α) = BotHom.id _ :=
  rfl

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

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

Разделы

Аффилиация

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