instLocPathConnectedSpace — Mathlib

English

Delta-generated spaces are locally path-connected.

Русский

Дельта-генерируемые пространства локально связаны по путям.

LaTeX

$$$$\text{LocPathConnectedSpace}(X)\quad\text{for } X \text{ with }\deltaGenerated\text{-topology}.$$$$

Lean4

/-- Delta-generated spaces are locally path-connected. -/
instance [DeltaGeneratedSpace X] : LocPathConnectedSpace X :=
  by
  rw [eq_deltaGenerated (X := X), deltaGenerated_eq_coinduced]
  exact LocPathConnectedSpace.coinduced _

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