X : Type u_1
Y : Type ?u.698693
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.698708
F : Set X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
X : Type u_1
Y : Type ?u.698693
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.698708
F : Set X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
case intro.intro.intro
X : Type u_1
Y : Type ?u.698693
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.698708
F : Set X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p ↑n)
t : Fin (n + 1) → ↑I
h : ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
X : Type u_1
Y : Type ?u.698693
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.698708
F : Set X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩
no goals
case intro.intro.intro
X : Type u_1
Y : Type ?u.698693
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.698708
F : Set X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p ↑n)
t : Fin (n + 1) → ↑I
h : ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
exact ⟨γ, t, h⟩
no goals
X : Type u_1
Y : Type ?u.698693
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.698708
F : Set X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ PathConnectedSpace X
infer_instance