ne_top_iff_exists — Mathlib

English

Let x be an element of WithTop(α). Then x ≠ ⊤ if and only if there exists a ∈ α such that x equals the embedding of a into WithTop(α).

Русский

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

LaTeX

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

Lean4

theorem ne_top_iff_exists {x : WithTop α} : x ≠ ⊤ ↔ ∃ a : α, ↑a = x :=
  Option.ne_none_iff_exists

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