pathConnectedSpace_iff_connectedSpace

English

If X is locally path-connected, then PathConnectedSpace X holds if and only if ConnectedSpace X holds. In other words, a locally path-connected space is path-connected exactly when it is connected.

Русский

Для локально путеподключенного пространства X выполняется: пространство или есть путевая связность, тогда и только тогда оно связано.

LaTeX

$$$\\text{PathConnectedSpace } X \\iff \\text{ConnectedSpace } X$$$

Lean4

theorem pathConnectedSpace_iff_connectedSpace : PathConnectedSpace X ↔ ConnectedSpace X :=
  by
  refine ⟨fun _ ↦ inferInstance, fun h ↦ ⟨inferInstance, fun x y ↦ ?_⟩⟩
  rw [← mem_pathComponent_iff, (IsClopen.pathComponent _).eq_univ] <;> simp

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