English
For a path γ and reparametrization f with f(0)=0 and f(1)=1, the range of γ.reparam f equals the range of γ.
Русский
Для траектории γ и переparametrизации f с f(0)=0 и f(1)=1 образ γ.reparam f равен образу γ.
LaTeX
$$$\operatorname{range}(\gamma.reparam(f, \cdots)) = \operatorname{range}(\gamma).$$$
Lean4
theorem range_reparam (γ : Path x y) {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
range (γ.reparam f hfcont hf₀ hf₁) = range γ :=
by
change range (γ ∘ f) = range γ
have : range f = univ := by
rw [range_eq_univ]
intro t
have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop
have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
· rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
rcases this t.2 with ⟨w, hw₁, hw₂⟩
rw [IccExtend_of_mem _ _ hw₁] at hw₂
exact ⟨_, hw₂⟩
rw [range_comp, this, image_univ]
