untopD_eq_untopD_iff — Mathlib

English

Equality of untopD(d, x) and untopD(d, y) is equivalent to either x=y or the pair (x=d, y=⊤) or (x=⊤, y=d).

Русский

Равенство untopD(d, x) и untopD(d, y) эквивалентно либо x=y, либо (x=d и y=⊤) либо (x=⊤ и y=d).

LaTeX

$$$\\mathrm{untopD}\,d\,x = \\mathrm{untopD}\,d\,y \\iff x = y \\lor (x = d \\land y = \\top) \\lor (x = \\top \\land y = d)$$$

Lean4

theorem untopD_eq_untopD_iff {d : α} {x y : WithTop α} :
    untopD d x = untopD d y ↔ x = y ∨ x = d ∧ y = ⊤ ∨ x = ⊤ ∧ y = d :=
  WithBot.unbotD_eq_unbotD_iff

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