withTopEquiv — Mathlib

English

Noncomputable equivalence between PartENat and ℕ∞ exists with toWithTop and its inverse.

Русский

Существует невычислимое эквивалентность между PartENat и ℕ∞ с помощью toWithTop и его обратной функции.

LaTeX

$$$\\\\text{withTopEquiv} : PartENat \\simeq \\mathbb{N}_{\\infty}$$$

Lean4

/-- `Equiv` between `PartENat` and `ℕ∞` (for the order isomorphism see
`withTopOrderIso`). -/
@[simps]
noncomputable def withTopEquiv : PartENat ≃ ℕ∞
    where
  toFun x := toWithTop x
  invFun x := ↑x
  left_inv x := by simp
  right_inv x := by simp

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