pathConnectedSpace_iff_univ — Mathlib

English

A PathConnectedSpace X implies IsPathConnected univ in X.

Русский

Связность по траекториям пространства X имплицирует, что множество X само по себе является путево связным.

LaTeX

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

Lean4

theorem pathConnectedSpace_iff_univ : PathConnectedSpace X ↔ IsPathConnected (univ : Set X) := by
  simp [pathConnectedSpace_iff, isPathConnected_iff, nonempty_iff_univ_nonempty]

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