X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range (↑γ ∘ f) = range ↑γ
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range ↑(reparam γ f hfcont hf₀ hf₁) = range ↑γ
change range (γ ∘ f) = range γ
no goals
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
this : range f = univ
⊢ range (↑γ ∘ f) = range ↑γ
rw [range_comp, this, image_univ]
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Surjective f
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range f = univ
rw [range_iff_surjective]
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
⊢ ∃ a, f a = t
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Surjective f
intro t
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
⊢ ∃ a, f a = t
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
⊢ ∃ a, f a = t
have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by continuity
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc (IccExtend (_ : 0 ≤ 1) f 0) (IccExtend (_ : 0 ≤ 1) f 1) ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
⊢ ∃ a, f a = t
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
⊢ ∃ a, f a = t
have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
no goals
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
⊢ Continuous (IccExtend (_ : 0 ≤ 1) f)
continuity
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc 0 1 ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
⊢ ∃ a, f a = t
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc (IccExtend (_ : 0 ≤ 1) f 0) (IccExtend (_ : 0 ≤ 1) f 1) ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
⊢ ∃ a, f a = t
rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
case intro.intro
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc 0 1 ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
w : ℝ
hw₁ : w ∈ Icc 0 1
hw₂ : IccExtend (_ : 0 ≤ 1) f w = t
⊢ ∃ a, f a = t
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc 0 1 ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
⊢ ∃ a, f a = t
rcases this t.2 with ⟨w, hw₁, hw₂⟩
case intro.intro
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc 0 1 ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
w : ℝ
hw₁ : w ∈ Icc 0 1
hw₂ : f { val := w, property := hw₁ } = t
⊢ ∃ a, f a = t
case intro.intro
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc 0 1 ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
w : ℝ
hw₁ : w ∈ Icc 0 1
hw₂ : IccExtend (_ : 0 ≤ 1) f w = t
⊢ ∃ a, f a = t
rw [IccExtend_of_mem _ _ hw₁] at hw₂
no goals
case intro.intro
X : Type u_1
Y : Type ?u.527823
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.527838
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend (_ : 0 ≤ 1) f)
this : Icc 0 1 ⊆ IccExtend (_ : 0 ≤ 1) f '' Icc 0 1
w : ℝ
hw₁ : w ∈ Icc 0 1
hw₂ : f { val := w, property := hw₁ } = t
⊢ ∃ a, f a = t
exact ⟨_, hw₂⟩