Locally constant functions on a preconnected set

A function that is locally constant along a preconnected set takes the same value everywhere on it. Mathlib's IsLocallyConstant.apply_eq_of_preconnectedSpace says this for a locally constant function on a preconnected space; the statement below is the relative form, for a preconnected subset s of an ambient space, with local constancy expressed by the 𝓝[s] neighbourhood filter rather than by passing to the subtype.

Main declarations

• IsPreconnected.apply_eq_of_eventually_eq: a function whose value is locally constant along a preconnected set is constant along it.

The example at the end of the file spells the statement out on the interval [0, 1] ⊆ ℝ, where it says that a map into a discrete space continuous on [0, 1] cannot take two different values there. That is the obstruction to extending a discrete-valued map off a closed subspace of a space that is not totally disconnected.

theorem IsPreconnected.apply_eq_of_eventually_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {f : X → Y} (hs : IsPreconnected s) (hf : ∀ t ∈ s, ∀ᶠ (u : X) in nhdsWithin t s, f u = f t) {a b : X} (ha : a ∈ s) (hb : b ∈ s) : f a = f b

A function that is locally constant along a preconnected set is constant along it.

This is IsLocallyConstant.apply_eq_of_preconnectedSpace transported to the subspace s.