pathConnectedSpace_iff_eq — Mathlib

English

A space X is PathConnectedSpace iff there exists x ∈ X with pathComponent x = univ.

Русский

Пространство X есть PathConnectedSpace тогда и только тогда, когда существует x ∈ X с pathComponent(x)=univ.

LaTeX

$$PathConnectedSpace X ↔ ∃ x : X, \mathrm{pathComponent}(x) = univ$$

Lean4

theorem pathConnectedSpace_iff_eq : PathConnectedSpace X ↔ ∃ x : X, pathComponent x = univ := by
  simp [pathConnectedSpace_iff_univ, isPathConnected_iff_eq]
    -- see Note [lower instance priority]

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