untop_eq_iff — Mathlib

English

For a non-top a ∈ WithTop α and b ∈ α, a.untop h = b iff a = ↑b (as elements of WithTop α).

Русский

Для не-верхнего a ∈ WithTop(α) и b ∈ α, a.untop h = b эквивалентно a = ↑b (как элементы WithTop(α)).

LaTeX

$$$a \neq \top \Rightarrow (a.untop h = b) \iff (a = \uparrow b)$$$

Lean4

theorem untop_eq_iff {a : WithTop α} {b : α} (h : a ≠ ⊤) : a.untop h = b ↔ a = b :=
  WithBot.unbot_eq_iff (α := αᵒᵈ) h

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