joinedIn — Mathlib

English

If F is path connected, then for any x ∈ F and y ∈ F, there is a path in F joining x to y.

Русский

Если F связно по траекториям, то для любых x,y ∈ F существует траектория внутри F, соединяющая x и y.

LaTeX

$$$$\forall x\in F\,\forall y\in F\,\text{JoinedIn }F\ x\ y.$$$$

Lean4

theorem joinedIn (h : IsPathConnected F) : ∀ᵉ (x ∈ F) (y ∈ F), JoinedIn F x y := fun _x x_in _y y_in =>
  let ⟨_b, _b_in, hb⟩ := h
  (hb x_in).symm.trans (hb y_in)

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