English
The operation of appending a function on Fin m and Fin n to get a function on Fin (m+n) is continuous.
Русский
Операция объединения функций на Fin m и Fin n в функцию на Fin (m+n) непрерывна.
LaTeX
$$$\forall m,n, \,\text{Continuous } (p: (Fin\,m \to X) \times (Fin\,n \to X) \to (Fin\,(m+n) \to X)) \\$$
Lean4
/-- The natural homeomorphism `(ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)`.
`Equiv.sumArrowEquivProdArrow` as a homeomorphism. -/
@[simps!]
def sumArrowHomeomorphProdArrow {ι ι' : Type*} : (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)
where
toEquiv := Equiv.sumArrowEquivProdArrow _ _ _
continuous_toFun := by
dsimp [Equiv.sumArrowEquivProdArrow]
fun_prop
continuous_invFun :=
continuous_pi fun i ↦
match i with
| .inl i => by apply (continuous_apply _).comp' continuous_fst
| .inr i => by apply (continuous_apply _).comp' continuous_snd
