English
Let s be path-connected and p: Fin(n+1) → X with p(i) ∈ s for all i. Then there exists a path γ from p(0) to p(last n) whose range lies in s.
Русский
Пусть s путево связано и p: Fin(n+1)→X с p(i)∈s для всех i. Тогда существует путь γ от p(0) к p(last n), чей образ лежит в s.
LaTeX
$$∃ γ : Path(p_0, p_{\mathrm{last}(n)}) , range(γ) ⊆ s ∧ ∀ i, p(i) ∈ range(γ)$$
Lean4
theorem exists_path_through_family {n : ℕ} {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X)
(hp : ∀ i, p i ∈ s) : ∃ γ : Path (p 0) (p (last n)), range γ ⊆ s ∧ ∀ i, p i ∈ range γ :=
by
cases p using snocCases with
| _ p x => ?_
simp only [forall_fin_succ', snoc_castSucc, snoc_last, Path.cast_coe, Path.target_mem_range, and_true] at hp ⊢
obtain ⟨hp, hx⟩ := hp
induction p using snocInduction generalizing x with
| h0 =>
simp only [snoc_zero]
use Path.refl x
simp [hx]
| @h n p y
hp₂ =>
simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
obtain ⟨hp, hy⟩ := hp
specialize hp₂ y hp hy
obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂
obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx
rw [← range_subset_iff] at hγ₁
use γ₀.trans γ₁
simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true, union_subset_iff]
tauto
