English
If a continuous map f from a connected space α into a disjoint union Σi X_i is given, then f factors through a single component: there exists an index i and a continuous g: α → X_i such that f = Σ i ∘ g.
Русский
Пусть f: α → Σ_i X_i непрерывна, α — связное пространство. Тогда существует индекс i и непрерывная карта g: α → X_i такая, что f = Σ i ∘ g.
LaTeX
$$$\exists i\, \exists g:\alpha \to X_i\, (Continuous\ g \land f = \Sigma_i \circ g)$$$
Lean4
/-- A continuous map from a connected space to a disjoint union `Σ i, X i` can be lifted to one of
the components `X i`. See also `ContinuousMap.exists_lift_sigma` for a version with bundled
`ContinuousMap`s. -/
theorem exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpace (X i)] {f : α → Σ i, X i} (hf : Continuous f) :
∃ (i : ι) (g : α → X i), Continuous g ∧ f = Sigma.mk i ∘ g :=
by
obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) :=
by
rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩
rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩
refine ⟨i, g, ?_, rfl⟩
rwa [← IsEmbedding.sigmaMk.continuous_iff] at hf
