lt_coe_succ_iff_le — Mathlib

English

For x ≠ ⊤ and n ∈ ℕ, x < n.succ.cast iff x ≤ n.cast.

Русский

Для x ≠ ⊤ и n ∈ ℕ, x < n.succ.cast эквивалентно x ≤ n.cast.

LaTeX

$$$ \forall x : \mathrm{PartENat}, \forall n : \mathbb{N}, x \neq \top \Rightarrow (x < n.succ.cast \iff x \le n.cast)$$$

Lean4

theorem lt_coe_succ_iff_le {x : PartENat} {n : ℕ} (hx : x ≠ ⊤) : x < n.succ ↔ x ≤ n := by
  rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, lt_add_one_iff_lt hx]

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