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