exists_path_through_family — Mathlib

English

In a path-connected space, for any p: Fin(n+1) → X, there exist γ and t with γ(t i) = p i for all i and γ(t) ⊆ X.

Русский

В пространстве, где есть путь между любыми двумя точками, существуют γ и t, удовлетворяющие γ(t i) = p i и γ(t) ⊆ X.

LaTeX

$$∃ γ : Path(p_0, p_last), ∃ t : Fin(n+1) → I, ∀ i, γ(t i) = p i$$

Lean4

theorem exists_path_through_family {n : ℕ} (p : Fin (n + 1) → X) : ∃ γ : Path (p 0) (p (last n)), ∀ i, p i ∈ range γ :=
  by
  have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
  rcases this.exists_path_through_family p fun _i => True.intro with ⟨γ, -, h⟩
  exact ⟨γ, h⟩

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