English
If f has constant germs at every point of a preconnected set s, then f is constant on s.
Русский
Если гёрмы f константны на каждой точке множества s, являющегося префинитически связным, то f константен на s.
LaTeX
$$$\forall s, (h : ∀ x \in s, (f : \mathrm{Germ}(\mathcal N x) Y).IsConstant) (hs : IsPreconnected s) \Rightarrow \forall x, x' \in s, f x = f x'$$$
Lean4
theorem eq_of_germ_isConstant_on {s : Set X} (h : ∀ x ∈ s, (f : Germ (𝓝 x) Y).IsConstant) (hs : IsPreconnected s)
{x' : X} (x_in : x ∈ s) (x'_in : x' ∈ s) : f x = f x' :=
by
let i : s → X := fun x ↦ x
change (f ∘ i) (⟨x, x_in⟩ : s) = (f ∘ i) (⟨x', x'_in⟩ : s)
have : PreconnectedSpace s := Subtype.preconnectedSpace hs
exact eq_of_germ_isConstant (fun y ↦ Germ.isConstant_comp_subtype (h y y.2)) _ _
