ofENat_le — Mathlib

English

The map toWithTop preserves addition: toWithTop(x + y) = toWithTop x + toWithTop y.

Русский

toWithTop сохраняет сложение: toWithTop(x + y) = toWithTop x + toWithTop y.

LaTeX

$$$\\\\operatorname{toWithTop}(x + y) = \\\\operatorname{toWithTop}(x) + \\\\operatorname{toWithTop}(y)$$$

Lean4

@[simp, norm_cast]
theorem ofENat_le {x y : ℕ∞} : ofENat x ≤ ofENat y ↔ x ≤ y := by
  classical rw [← toWithTop_le, toWithTop_ofENat, toWithTop_ofENat]

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