Continuous maps from preconnected spaces into disjoint unions

Each summand Y j of a disjoint union Σ j, Y j is clopen, so a continuous map out of a preconnected space lands in a single summand. This needs no nonemptiness assumption, unlike Continuous.exists_lift_sigma, which lifts a map out of a connected space.

Main declarations

• Continuous.fst_apply_eq_fst_apply: a continuous map from a preconnected space into Σ j, Y j sends all points into the same summand.

theorem Continuous.fst_apply_eq_fst_apply {α : Type u_1} {κ : Type u_2} {Y : κ → Type u_3} [TopologicalSpace α] [(j : κ) → TopologicalSpace (Y j)] [PreconnectedSpace α] {f : α → (j : κ) × Y j} (hf : Continuous f) (a b : α) : (f a).fst = (f b).fst

A continuous map from a preconnected space into a disjoint union lands in a single summand: any two points have images in the same summand.