ofNat — Mathlib

English

The map ofNat: Nat → Bool sends 0 to false and every positive number to true.

Русский

Преобразование ofNat: Натуральное число → Булево отображает 0 в false, а положительные числа в true.

LaTeX

$$$ \forall n : \mathbb{N},\; \text{ofNat}(n) = \text{true} \iff n \neq 0 $$$

Lean4

/-- convert a `ℕ` to a `Bool`, `0 -> false`, everything else -> `true` -/
def ofNat (n : Nat) : Bool :=
  decide (n ≠ 0)

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