coe_succ_le_iff — Mathlib

English

For any n ∈ ℕ and e ∈ PartENat, ↑(n+1) ≤ e iff ↑n < e.

Русский

Для любого n∈ℕ и e∈PartENat, ↑(n+1) ≤ e эквивалентно ↑n < e.

LaTeX

$$$ \forall n : \mathbb{N}, \forall e : \mathrm{PartENat}, \uparrow(n+1) \le e \iff \uparrow n < e $$$

Lean4

theorem coe_succ_le_iff {n : ℕ} {e : PartENat} : ↑n.succ ≤ e ↔ ↑n < e := by
  rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, add_one_le_iff_lt (natCast_ne_top n)]

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