6.15. MappingDegree.ClopennessOfLocallyConstDischarge🔗

Jacobians.MappingDegree.ClopennessOfLocallyConstDischarge — source

clopennessOfLocallyConst_holds

Discharge of ClopennessOfLocallyConstHypothesis. The locally-constant locus S = {x | ∀ᶠ x' in 𝓝 x, f x' = y₀} of a C^ω map f : X → Y is closed.

The proof is the chart-local identity theorem: at any closure point x of S, continuity + T2 already forces f x = y₀; analyticity of the chart pullback on a preconnected open ball, combined with eventual equality at a witness point of S inside the ball, propagates constancy across the ball and hence to a neighbourhood of x.

theorem clopennessOfLocallyConst_holds
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] :
    ClopennessOfLocallyConstHypothesis X Y