withTopOrderIso — Mathlib

English

There is an order isomorphism between PartENat and ℕ∞ given by withTopEquiv, i.e., PartENat ≃o ℕ∞.

Русский

Существует порядок-изоморфизм между PartENat и ℕ∞, задаваемый отображением withTopEquiv.

LaTeX

$$$ PartENat \cong_o \mathbb{N}_\infty $$$

Lean4

/-- `toWithTop` induces an order isomorphism between `PartENat` and `ℕ∞`. -/
noncomputable def withTopOrderIso : PartENat ≃o ℕ∞ :=
  { withTopEquiv with map_rel_iff' := @fun _ _ => withTopEquiv_le }

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