exists_path_through_family' — Mathlib

English

As above, but with γ and t such that γ(t i) = p i for all i.

Русский

Как выше, но существует γ и t such that γ(t i) = p i для всех i.

LaTeX

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

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))) (t : Fin (n + 1) → I), (∀ t, γ t ∈ s) ∧ ∀ i, γ (t i) = p i :=
  by
  rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩
  rcases hγ with ⟨h₁, h₂⟩
  simp only [range, mem_setOf_eq] at h₂
  rw [range_subset_iff] at h₁
  choose! t ht using h₂
  exact ⟨γ, t, h₁, ht⟩

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