ne_top_iff_dom — Mathlib

English

For any x in PartENat, x ≠ ⊤ if and only if x has a finite domain (i.e., x equals some natural cast).

Русский

Для любого x из PartENat, x ≠ ⊤ эквивалентно тому, что у x есть конечный домен (то есть x = n для некоторого n ∈ ℕ).

LaTeX

$$$ x \ne \top \iff x \in \mathrm{Dom} \quad$ (equivalently, $\exists n \in \mathbb{N}, x = n$)$$

Lean4

theorem ne_top_iff_dom {x : PartENat} : x ≠ ⊤ ↔ x.Dom := by classical exact not_iff_comm.1 Part.eq_none_iff'.symm

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