toNat_le_of_le_coe — Mathlib

English

If m ≤ n for ENat m and finite natural n, then toNat m ≤ n.

Русский

Если m ≤ n для ENat m и конечного n, то toNat m ≤ n.

LaTeX

$$$\\\\forall m \\\\in \\\\mathbb{N}_{\\\\infty}, \\\\forall n \\\\in \\\\mathbb{N}, \\\\operatorname{toNat}(m) \\\\le n \\\\text{ при } m \\\\le n$$$

Lean4

theorem toNat_le_of_le_coe {m : ℕ∞} {n : ℕ} (h : m ≤ n) : toNat m ≤ n :=
  by
  lift m to ℕ using ne_top_of_le_ne_top (coe_ne_top n) h
  simpa using h

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