isPathConnected — Mathlib

English

A star-shaped set with respect to a point a ∈ s is path-connected; any two points can be joined by a path staying in s.

Русский

Звездообразное множество относительно точки a ∈ s взаимосвязано по пути; любые две точки можно соединить путём, лежащим внутри множества.

LaTeX

$$$ IsPathConnected\ s $ if $ s \text{ is StarConvex around } a \text{ and } a \in s $.$$

Lean4

protected theorem isPathConnected {s : Set E} {a : E} (h : StarConvex ℝ a s) (ha : a ∈ s) : IsPathConnected s :=
  ⟨a, ha, fun _y hy ↦ .of_segment_subset <| h.segment_subset hy⟩

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