English
If h is continuous and g is a map with g ∘ inclusion = f, then g equals the lift of f, i.e., g = h.connectedComponentsLift.
Русский
Если h непрерывно и g удовлетворяет g ∘ включение = f, то g равен лифту отображения f: g = h.connectedComponentsLift.
LaTeX
$$$(g \circ (\\iota) = f) \Rightarrow g = h.\\text{connectedComponentsLift}$$$
Lean4
/-- A version of `IsPreconnected.constant_of_mapsTo` that assumes that the codomain is nonempty and
proves that `f` is equal to `const α y` on `S` for some `y ∈ T`. -/
theorem eqOn_const_of_mapsTo {S : Set α} (hS : IsPreconnected S) {β} [TopologicalSpace β] {T : Set β}
[DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) (hne : T.Nonempty) :
∃ y ∈ T, EqOn f (const α y) S :=
by
rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)
· exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩
· exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hc hTm hx' hx⟩
