continuous_append — Mathlib

English

There is a natural homeomorphism between (Fin m → X) × (Fin n → X) and Fin (m+n) → X given by the appendEquiv.

Русский

Существуют естественный гомеоморфизм между (Fin m → X) × (Fin n → X) и Fin (m+n) → X, задаваемый appendEquiv.

LaTeX

$$$ (Fin m \to X) \times (Fin n \to X) \cong_{Top} Fin (m+n) \to X \text{ via } Fin.appendEquiv m n.$$$

Lean4

theorem _root_.Fin.continuous_append (m n : ℕ) : Continuous fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2 :=
  by
  suffices Continuous (Fin.appendEquiv m n) by exact this
  rw [Fin.appendEquiv_eq_homeomorph]
  exact Homeomorph.continuous_toFun _

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