untopD_eq_iff — Mathlib

English

There is a precise equivalence describing when two applications of untopD agree, reflecting the three-way cases (x=y, x=d and y=top, or x=top and y=d).

Русский

Существует точное эквивалентное соотношение для равенства двух значений untopD, учитывающее три случая: x=y, x=d и y=⊤, или x=⊤ и y=d.

LaTeX

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

Lean4

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

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