insertAt — Mathlib

English

The backward direction of the homeomorphism between I^N and I × I^{N\setminus {i}}.

Русский

Обратное направление гомеоморфизма между I^N и I × I^{N\setminus {i}}.

LaTeX

$$insertAt(i) : (I × I^{ j // j ≠ i }) ≃ₜ I^N$$

Lean4

/-- The backward direction of the homeomorphism
  between the cube $I^N$ and $I × I^{N\setminus\{j\}}$. -/
abbrev insertAt (i : N) : (I × I^{ j // j ≠ i }) ≃ₜ I^N :=
  (funSplitAt I i).symm

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