pathComponent — Mathlib

English

In a locally path connected space, each path component is clopen.

Русский

В локально путепроходимом пространстве каждая путепроходящая компонента клипна (одновременно открыта и замкнута).

LaTeX

$$IsClopen\pathComponent x$$

Lean4

/-- In a locally path connected space, each path component is a clopen set. -/
protected theorem pathComponent (x : X) : IsClopen (pathComponent x) :=
  ⟨.pathComponent x, .pathComponent x⟩

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