ne_top_iff_exists — Mathlib

English

There exists a finite ENat number not equal to ⊤ if and only if there exists a natural m such that ↑m = n.

Русский

Существование конечного элемента ENat, отличного от ⊤, эквивалентно существованию натурального m, такого что ↑m = n.

LaTeX

$$$n \neq \top \leftrightarrow \exists m : \mathbb{N}, (m : ENat) = n$$$

Lean4

theorem ne_top_iff_exists : n ≠ ⊤ ↔ ∃ m : ℕ, ↑m = n :=
  WithTop.ne_top_iff_exists

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