ofENat_mono — Mathlib

English

The inclusion ENat → Cardinal is order-preserving: if m ≤ n for m,n ∈ ℕ∞, then ofENat m ≤ ofENat n.

Русский

Отображение из ℕ∞ в Кардиналы сохраняет порядок: если m ≤ n для m,n ∈ ℕ∞, то ofENat(m) ≤ ofENat(n).

LaTeX

$$$\forall m,n \in \mathbb{N}_\infty,\ m \le n \Rightarrow \operatorname{ofENat}(m) \le \operatorname{ofENat}(n)$$$

Lean4

theorem ofENat_mono : Monotone ofENat :=
  ofENat_strictMono.monotone

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