isPathConnected_iff — Mathlib

English

Path-connectedness of F is equivalent to F being nonempty and every pair of points in F being joined in F.

Русский

Связность по траекториям F эквивалентна тому, что F непусто и любая пара точек в F соединяется траекторией внутри F.

LaTeX

$$$$\IsPathConnected F \iff F \neq \emptyset \land \forall x\in F\, \forall y\in F\,\JoinedIn F\ x y.$$$$

Lean4

theorem isPathConnected_iff : IsPathConnected F ↔ F.Nonempty ∧ ∀ᵉ (x ∈ F) (y ∈ F), JoinedIn F x y :=
  ⟨fun h =>
    ⟨let ⟨b, b_in, _hb⟩ := h;
      ⟨b, b_in⟩,
      h.joinedIn⟩,
    fun ⟨⟨b, b_in⟩, h⟩ => ⟨b, b_in, h _ b_in⟩⟩

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