unbotD_eq_unbotD_iff — Mathlib

English

unbotD d x = unbotD d y iff x = y or (x = d and y = ⊥) or (x = ⊥ and y = d).

Русский

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

LaTeX

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

Lean4

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

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