ofENat_le_nat — Mathlib

English

Let m ∈ ℕ∞ and n ∈ ℕ. Then the natural embedding of ENat into cardinals preserves order with respect to natural numbers: ofENat(m) ≤ n if and only if m ≤ n.

Русский

Пусть m ∈ ℕ∞ и n ∈ ℕ. Тогда естественное включение ENat в кардиналы сохраняет порядок по отношению к n: ofENat(m) ≤ n тогда и только тогда, когда m ≤ n.

LaTeX

$$$\forall m : \mathbb{N}_\infty, \forall n : \mathbb{N},\; \operatorname{ofENat}(m) \le n \iff m \le n$$$

Lean4

@[simp]
theorem ofENat_le_nat {m : ℕ∞} {n : ℕ} : ofENat m ≤ n ↔ m ≤ n := by norm_cast

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