English
If two maps g1,g2: ConnectedComponents(α) → β agree on α via the canonical inclusion, then g1 = g2.
Русский
Если два отображения g1,g2: ConnectedComponents(α) → β совпадают на α через каноническое включение, то g1 = g2.
LaTeX
$$$g_1 \circ (↑) = g_2 \circ (↑) \Rightarrow g_1 = g_2$$$
Lean4
/-- Refinement of `IsPreconnected.constant` only assuming the map factors through a
discrete subset of the target. -/
theorem constant_of_mapsTo {S : Set α} (hS : IsPreconnected S) {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T]
{f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y :=
by
let F : S → T := hTm.restrict f S T
suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this
exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.mapsToRestrict _)
