listEquivSelfOfEquivNat — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall \\alpha\\,\\big(\\exists e:\\alpha\\simeq\\mathbb{N}\\big)\\Rightarrow \\text{List }\\alpha \\simeq \\alpha.$$$

Lean4

/-- If `α` is equivalent to `ℕ`, then `List α` is equivalent to `α`. -/
def listEquivSelfOfEquivNat {α : Type*} (e : α ≃ ℕ) : List α ≃ α :=
  calc
    List α ≃ List ℕ := listEquivOfEquiv e
    _ ≃ ℕ := listNatEquivNat
    _ ≃ α := e.symm

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