isPathConnected_iff_eq — Mathlib

English

A set F is path connected iff it is nonempty and any two points of F can be joined by a path within F.

Русский

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

LaTeX

$$$$\IsPathConnected(F) \iff F\neq\varnothing \land \forall x\in F\,\forall y\in F\,\JoinedIn F\ x y.$$$$

Lean4

theorem isPathConnected_iff_eq : IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F :=
  by
  constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in
  · ext y
    exact ⟨fun hy => hy.mem.2, @h _⟩
  · intro y y_in
    rwa [← h] at y_in

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