natCast_lt_of_coe_top_le_withTop — Mathlib

English

If top ≤ N for N ∈ WithTop ENat, then n < N for every natural n.

Русский

Если верха ≤ N, то для каждого натурального n выполняется n < N.

LaTeX

$$$$\forall N \in \mathrm{WithTop}(\mathbb{N}_\infty),\ (\top : \mathbb{N}_\infty) \le N \Rightarrow \forall n \in \mathbb{N},\ n < N.$$$$

Lean4

theorem natCast_lt_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : (⊤ : ℕ∞) ≤ N) (n : ℕ) : n < N :=
  lt_of_lt_of_le (mod_cast lt_add_one n) (natCast_le_of_coe_top_le_withTop hN (n + 1))

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