natSumNatEquivNat — Mathlib

English

If α has an equivalence with ℕ, then α × α is equivalent to α.

Русский

Если у α есть эквивалентность с ℕ, то α × α эквивалентно α.

LaTeX

$$$\\bigl(\\alpha \\times \\alpha\\bigr) \\simeq \\alpha \\quad\\text{given } e:\\alpha \\simeq \\mathbb{N}. $$$

Lean4

/-- An equivalence between `ℕ ⊕ ℕ` and `ℕ`, by mapping `(Sum.inl x)` to `2 * x` and `(Sum.inr x)` to
`2 * x + 1`.
-/
@[simps! symm_apply]
def natSumNatEquivNat : ℕ ⊕ ℕ ≃ ℕ :=
  (boolProdEquivSum ℕ).symm.trans boolProdNatEquivNat

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