piFinTwo — Mathlib

English

There is a homeomorphism between (Fin 2 → X) and X × X, given by f ↦ (f(0), f(1)).

Русский

Существует гомеоморфизм между (Fin 2 → X) и X × X, задаваемый f ↦ (f(0), f(1)).

LaTeX

$$$ (Fin 2 \to X) \cong_{Top} X \times X \\ (f \mapsto (f(0), f(1))). $$$

Lean4

/-- Homeomorphism between dependent functions `Π i : Fin 2, X i` and `X 0 × X 1`. -/
@[simps! -fullyApplied]
def piFinTwo.{u} (X : Fin 2 → Type u) [∀ i, TopologicalSpace (X i)] : (∀ i, X i) ≃ₜ X 0 × X 1
    where
  toEquiv := piFinTwoEquiv X
  continuous_toFun := (continuous_apply 0).prodMk (continuous_apply 1)
  continuous_invFun := continuous_pi <| Fin.forall_fin_two.2 ⟨continuous_fst, continuous_snd⟩

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