Constancy of a linear image of a curve #
A curve whose derivative on a closed interval is killed by a continuous linear map has constant image under that map on that interval.
Main results #
ContinuousLinearMap.apply_eq_apply_left_of_hasDerivWithinAt: the image under a continuous linear map of such a curve agrees with its value at the left endpoint.
theorem
ContinuousLinearMap.apply_eq_apply_left_of_hasDerivWithinAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(L : E →L[ℝ] F)
{γ γ' : ℝ → E}
{a b : ℝ}
(h : ∀ t ∈ Set.Icc a b, HasDerivWithinAt γ (γ' t) (Set.Icc a b) t)
(h₁ : ∀ t ∈ Set.Icc a b, L (γ' t) = 0)
{t : ℝ}
(ht : t ∈ Set.Icc a b)
:
A curve whose derivative on a closed interval is sent to zero by a continuous linear map L
has constant image under L on that interval.