of_constant_on_preconnected_clopens

English

If X is LocallyConnected and f is constant on every preconnected clopen subset, then f is locally constant.

Русский

Если X локально связно и f константен на каждом предсоединённом открыто-закрытом множестве, то f локально константна.

LaTeX

$$IsLocallyConstant f$$

Lean4

theorem of_constant_on_preconnected_clopens [LocallyConnectedSpace X] {f : X → Y}
    (h : ∀ U : Set X, IsPreconnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x) : IsLocallyConstant f :=
  of_constant_on_connected_clopens fun U hU ↦ h U hU.isPreconnected

Похожие утверждения