unbotD_eq_iff

Mathlib.Order.WithBot

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

English

unbotD d x = y iff x = y or x = ⊥ and y = d

Русский

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

LaTeX

$$$\\mathrm{Eq}(\\mathrm{WithBot.unbotD}\\, d\\, x, y) \\iff (x=y) \\lor (x=\\bot \\land y=d)$$$

Lean4

theorem unbotD_eq_iff {d y : α} {x : WithBot α} : unbotD d x = y ↔ x = y ∨ x = ⊥ ∧ y = d := by
  induction x <;> simp [@eq_comm _ d]

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

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

Разделы

Аффилиация

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