ofENat_le_ofNat — Mathlib

English

Let m ∈ ENat and n ∈ ℕ with AtLeastTwo. Then ofENat(m) ≤ ofNat(n) in Cardinals if and only if m ≤ OfNat.ofNat(n) in ENat.

Русский

Пусть m ∈ ENat и n ∈ ℕ с условием AtLeastTwo. Тогда ofENat(m) ≤ ofNat(n) в кардиналах эквивалентно m ≤ OfNat.ofNat(n) в ENat.

LaTeX

$$$\forall m : \mathbb{N}_\infty, \forall n : \mathbb{N}, [n.\AtLeastTwo],\; \operatorname{ofENat}(m) \le \operatorname{ofNat}(n) \iff m \le \operatorname{OfNat}.ofNat(n)$$$

Lean4

@[simp]
theorem ofENat_le_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : ofENat m ≤ ofNat(n) ↔ m ≤ OfNat.ofNat n :=
  ofENat_le_nat

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