isConnected_iff_isPathConnected — Mathlib

English

For an open subset U of a locally path-connected space X, U is connected if and only if U is path-connected.

Русский

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

LaTeX

$$IsOpen U → (IsConnected U ↔ IsPathConnected U)$$

Lean4

theorem isConnected_iff_isPathConnected {U : Set X} (U_op : IsOpen U) : IsConnected U ↔ IsPathConnected U :=
  by
  rw [isConnected_iff_connectedSpace, isPathConnected_iff_pathConnectedSpace]
  haveI := U_op.locPathConnectedSpace
  exact pathConnectedSpace_iff_connectedSpace.symm

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