unbotD_eq_self_iff

Mathlib.Order.WithBot

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

English

unbotD d x = d iff x = d or x = ⊥.

Русский

unbotD d x = d эквивалентно x = d или x = ⊥.

LaTeX

$$$\\mathrm{unbotD}\\, d\\, x = d \\iff x = d \\lor x=\\bot$$$

Lean4

@[simp]
theorem unbotD_eq_self_iff {d : α} {x : WithBot α} : unbotD d x = d ↔ x = d ∨ x = ⊥ := by simp [unbotD_eq_iff]

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

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

Разделы

Аффилиация

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