withTopAddEquiv — Mathlib

English

There is an additive monoid isomorphism between PartENat and ℕ∞ extending the top map, i.e., withTopAddEquiv : PartENat ≃+ ℕ∞.

Русский

Существует аддитивное моноидальное изоморфизм между PartENat и ℕ∞, расширяющее отображение верхнего элемента.

LaTeX

$$$ PartENat \cong_+ \mathbb{N}_\infty $$$

Lean4

/-- `toWithTop` induces an additive monoid isomorphism between `PartENat` and `ℕ∞`. -/
noncomputable def withTopAddEquiv : PartENat ≃+ ℕ∞ :=
  { withTopEquiv with
    map_add' := fun x y => by
      simp only [withTopEquiv]
      exact toWithTop_add }

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