English
To give a continuous map out of a disjoint union is the same as giving a continuous map out of each term. This is the Sigma.uncurry for continuous maps.
Русский
Задать непрерывное отображение из дизъюнкта эквивалентно заданию непрерывного отображения из каждого слагаемого. Это Sigma.uncurry для непрерывных отображений.
LaTeX
$$$\sigma: (\forall i, C(X_i,A)) \to C((\Sigma i, X_i), A),\qquad \sigma(f)(\langle i,x\rangle)=f(i)(x)$$$
Lean4
/-- To give a continuous map out of a disjoint union, it suffices to give a continuous map out of
each term. This is `Sigma.uncurry` for continuous maps.
-/
@[simps]
def sigma (f : ∀ i, C(X i, A)) : C((Σ i, X i), A) where toFun ig := f ig.fst ig.snd
