natCast_le_of_coe_top_le_withTop — Mathlib

English

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

Русский

Если верха ≤ N для N ∈ WithTop ENat, то 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 \le N.$$$$

Lean4

theorem natCast_le_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : (⊤ : ℕ∞) ≤ N) (n : ℕ) : n ≤ N :=
  le_trans (mod_cast le_top) hN

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