mem_range_succ — Mathlib

English

For natural numbers i, i ∈ range Nat.succ iff 0 < i.

Русский

Для натурального i выполняется, что i принадлежит диапазону successor, тогда и только тогда, когда i > 0.

LaTeX

$$$ i \\in \\operatorname{range} (\\operatorname{Nat.succ}) \\;\\iff\\; 0 < i $$$

Lean4

theorem _root_.Nat.mem_range_succ (i : ℕ) : i ∈ range Nat.succ ↔ 0 < i :=
  ⟨by grind, fun h => ⟨_, Nat.succ_pred_eq_of_pos h⟩⟩

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