prodEquivOfEquivNat — Mathlib

English

If α is equivalent to ℕ, then α × α is equivalent to α.

Русский

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

LaTeX

$$$(\\alpha \\times \\alpha) \\simeq \\alpha$ от эквивелентности $e: \\alpha \\simeq \\mathbb{N}$.$$

Lean4

/-- An equivalence between `α × α` and `α`, given that there is an equivalence between `α` and `ℕ`.
-/
def prodEquivOfEquivNat (e : α ≃ ℕ) : α × α ≃ α :=
  calc
    α × α ≃ ℕ × ℕ := prodCongr e e
    _ ≃ ℕ := pairEquiv
    _ ≃ α := e.symm

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