ofDual_apply_top

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.ofDual_apply_top

English

Applying the duality to the top element of WithTop(α) yields the bottom element.

Русский

При применении дуальности к вершине WithTop(α) получается нижняя вершина.

LaTeX

$$$\\mathrm{WithTop}.\\mathrm{ofDual}(\\top) = \\bot$$$

Lean4

@[simp]
theorem ofDual_apply_top : WithTop.ofDual (⊤ : WithTop α) = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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