add_one_natCast_le_withTop_of_lt — Mathlib

English

For m ∈ ℕ and n ∈ WithTop ENat, if m < n, then (m+1) cast ≤ n.

Русский

Для m ∈ ℕ и n ∈ WithTop ENat, если m < n, то (m+1).cast ≤ n.

LaTeX

$$$$\forall m \in \mathbb{N},\forall n \in \mathrm{WithTop}(\mathbb{N}_\infty),\ m < n \Rightarrow (m + 1)\;\text{cast} \le n.$$$$

Lean4

theorem add_one_natCast_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : m < n) : (m + 1 : ℕ) ≤ n := by
  match n with
  | ⊤ => exact le_top
  | (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
  | (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h

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