eq_top_iff_forall_ne — Mathlib

English

Let x be an element of WithTop(α). Then x = ⊤ if and only if for every a ∈ α, the embedded a is not equal to x.

Русский

Пусть x ∈ WithTop(α). Тогда x = ⊤ тогда и только тогда, когда для каждого a ∈ α имеет место, что ↑a ≠ x.

LaTeX

$$$\forall x : \mathrm{WithTop}(\alpha),\ x = \top \iff \forall a : \alpha, \uparrow a \neq x$$$

Lean4

theorem eq_top_iff_forall_ne {x : WithTop α} : x = ⊤ ↔ ∀ a : α, ↑a ≠ x :=
  Option.eq_none_iff_forall_some_ne

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