of_constant_on_connected_components

English

If X is LocallyConnected and f is constant on each connected component, then f is locally constant.

Русский

Если XLocallyConnected и f константен на каждой связной компоненте, то f локально константна.

LaTeX

$$IsLocallyConstant f$$

Lean4

theorem of_constant_on_connected_components [LocallyConnectedSpace X] {f : X → Y}
    (h : ∀ x, ∀ y ∈ connectedComponent x, f y = f x) : IsLocallyConstant f :=
  (iff_exists_open _).2 fun x => ⟨connectedComponent x, isOpen_connectedComponent, mem_connectedComponent, h x⟩

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