isConnected — Mathlib

English

A path-connected set is connected.

Русский

Путь-связное множество является связным.

LaTeX

$$IsPathConnected F → IsConnected F$$

Lean4

/-- A path-connected set is connected.

(See `Counterexamples.TopologistsSineCurve` for the standard counterexample showing that the
converse is false.) -/
theorem isConnected (hF : IsPathConnected F) : IsConnected F :=
  by
  rw [isConnected_iff_connectedSpace]
  rw [isPathConnected_iff_pathConnectedSpace] at hF
  exact @PathConnectedSpace.connectedSpace _ _ hF

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