toDualTopEquiv_symm_coe

Mathlib.Order.Hom.WithTopBot

URI: https://scilib.ai/kg/mathlib#WithBot.toDualTopEquiv_symm_coe

English

The embedding α ↪o WithBot α is an order embedding preserving order.

Русский

Вложение α → WithBot α является упорядоченным вложением, сохраняющим порядок.

LaTeX

$$$\\text{OrderEmbedding}(\\alpha \\hookrightarrow \\mathrm{WithBot}\\alpha)$$$

Lean4

@[simp]
theorem toDualTopEquiv_symm_coe [LE α] (a : α) : WithBot.toDualTopEquiv.symm (toDual (a : WithTop α)) = ↑(toDual a) :=
  rfl

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

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

Разделы

Аффилиация

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