exists_path_through_family' — Mathlib

English

In a path-connected space, there exist γ and t such that γ(t i) = p i for all i and γ(t) ⊆ s.

Русский

В путево связном пространстве существуют γ и t, удовлетворяющие γ(t i) = p i и γ(t) ⊆ s.

LaTeX

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

Lean4

theorem exists_path_through_family' {n : ℕ} (p : Fin (n + 1) → X) :
    ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → I), ∀ i, γ (t i) = p i :=
  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 ⟨γ, t, -, h⟩
  exact ⟨γ, t, h⟩

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