untopD_eq_self_iff

Mathlib.Order.WithBot

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

English

The value of untopD equals d exactly when x equals d or x equals ⊤.

Русский

Значение unTopD равно d тогда и только тогда, когда x равно d или x равно ⊤.

LaTeX

$$$\\mathrm{untopD}\,d\,x = d \\iff x = d \\lor x = \\top$$$

Lean4

@[simp]
theorem untopD_eq_self_iff {d : α} {x : WithTop α} : untopD d x = d ↔ x = d ∨ x = ⊤ :=
  WithBot.unbotD_eq_self_iff

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

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

Разделы

Аффилиация

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