connectedComponentIn — Mathlib

English

For a locally connected space, if F is open then connectedComponentIn F x is open.

Русский

Для локально связанного пространства, если F открыто, то connectedComponentIn F x открыто.

LaTeX

$$IsOpen.connectedComponentIn$$

Lean4

protected theorem connectedComponentIn [LocallyConnectedSpace α] {F : Set α} {x : α} (hF : IsOpen F) :
    IsOpen (connectedComponentIn F x) := by
  rw [isOpen_iff_mem_nhds]
  intro y hy
  rw [connectedComponentIn_eq hy]
  exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

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