pathComponent — Mathlib

English

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

Русский

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

LaTeX

$$IsOpen\pathComponent x$$

Lean4

/-- In a locally path connected space, each path component is an open set. -/
protected theorem pathComponent (x : X) : IsOpen (pathComponent x) :=
  by
  rw [← pathComponentIn_univ]
  exact isOpen_univ.pathComponentIn _

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