isPathConnected_iff_pathConnectedSpace

English

A space X is PathConnected iff IsPathConnected univ in X.

Русский

Пространство X является PathConnected тогда и только тогда, когда univ в X является IsPathConnected.

LaTeX

$$PathConnectedSpace X ↔ IsPathConnected (univ : Set X)$$

Lean4

theorem isPathConnected_iff_pathConnectedSpace : IsPathConnected F ↔ PathConnectedSpace F := by
  rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ, Subtype.range_val_subtype,
    setOf_mem_eq]

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