ofENat_lt — Mathlib

English

The embedding of ENat into PartENat preserves order: for x,y ∈ ENat, ofENat x < ofENat y if and only if x < y.

Русский

Встраивание ENat в PartENat сохраняет порядок: для x,y ∈ ENat, ofENat x < ofENat y тогда и только тогда, когда x < y.

LaTeX

$$$\\forall {x,y : \\mathbb{N}_\\infty},\\; \\operatorname{ofENat}(x) < \\operatorname{ofENat}(y) \\iff x < y$$$

Lean4

@[simp, norm_cast]
theorem ofENat_lt {x y : ℕ∞} : ofENat x < ofENat y ↔ x < y := by
  classical rw [← toWithTop_lt, toWithTop_ofENat, toWithTop_ofENat]

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