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⟩⟩