splitAt — Mathlib

English

For each i ∈ N there is a canonical homeomorphism between I^N and I × I^{N\setminus {i}} splitting the i-th coordinate.

Русский

Для каждого i ∈ N существует каноническое гомеоморфизм между I^N и I × I^{N\setminus {i}}, разбиющий i-ю координату.

LaTeX

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

Lean4

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

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