one_le_iff_ne_zero_withTop — Mathlib

English

For any n ∈ WithTop ENat, 1 ≤ n if and only if n ≠ 0.

Русский

Для любого n ∈ WithTop ENat, 1 ≤ n тогда и только тогда, когда n ≠ 0.

LaTeX

$$$$\forall n \in \mathrm{WithTop}(\mathbb{N}_\infty),\ 1 \le n \iff n \ne 0.$$$$

Lean4

theorem one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} : 1 ≤ n ↔ n ≠ 0 :=
  ⟨fun h ↦ (zero_lt_one.trans_le h).ne', fun h ↦ add_one_natCast_le_withTop_of_lt (pos_iff_ne_zero.mpr h)⟩

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