IsPathConnected — Mathlib

English

A set F is path connected if it contains a point that can be joined to every other point in F.

Русский

Множество F является связным по траекториям, если в нем содержится точка, соединяющаяся траекторией с любой другой точкой из F.

LaTeX

$$$$\operatorname{IsPathConnected}(F) \iff \exists x\in F\,\forall y\in F\,\text{JoinedIn }F\, x\, y.$$$$

Lean4

/-- A set `F` is path connected if it contains a point that can be joined to all other in `F`. -/
def IsPathConnected (F : Set X) : Prop :=
  ∃ x ∈ F, ∀ ⦃y⦄, y ∈ F → JoinedIn F x y

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