instPathConnectedSpace — Mathlib

English

Every contractible space is path-connected.

Русский

Каждое конрактное пространство связано путями.

LaTeX

$$$\operatorname{PathConnectedSpace}(X)\text{ whenever } \operatorname{ContractibleSpace}(X).$$$

Lean4

instance (priority := 100) [ContractibleSpace X] : PathConnectedSpace X :=
  by
  obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X
  have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩
  rw [pathConnectedSpace_iff_eq]; use p; ext; tauto

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