toWithTop_add — Mathlib

English

There is a bijective correspondence between PartENat and ℕ∞ given by toWithTop and its inverse ofENat.

Русский

Существует биекция между PartENat и ℕ∞, задаваемая отображениями toWithTop и обратным via ofENat.

LaTeX

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

Lean4

@[simp]
theorem toWithTop_add {x y : PartENat} : toWithTop (x + y) = toWithTop x + toWithTop y := by
  refine PartENat.casesOn y ?_ ?_ <;> refine PartENat.casesOn x ?_ ?_ <;> simp [add_top, top_add, ← Nat.cast_add]

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