ne_top_iff — Mathlib

English

Let x be an element of PartENat. Then x is not the top element if and only if there exists a natural number n with x = n.

Русский

Пусть x принадлежит PartENat. Тогда x ≠ ⊤ тогда же, когда существует натуральное число n такое, что x = n.

LaTeX

$$$ x \ne \top \iff \exists n \in \mathbb{N}, x = n $$$

Lean4

theorem ne_top_iff {x : PartENat} : x ≠ ⊤ ↔ ∃ n : ℕ, x = n := by simpa only [← some_eq_natCast] using Part.ne_none_iff

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