tangentMapWithin_congr — Mathlib

English

If x and x' are the same point, then the MF derivative at x equals the MF derivative at x'.

Русский

Если точки x и x' совпадают, то MF-дифференциал в x равен MF-дифференциалу в x'.

LaTeX

$$$x'=x \\Rightarrow mfderiv I I' f x = mfderiv I I' f x'$$$

Lean4

theorem tangentMapWithin_congr (h : ∀ x ∈ s, f x = f₁ x) (p : TangentBundle I M) (hp : p.1 ∈ s) :
    tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s p :=
  by
  refine TotalSpace.ext (h p.1 hp) ?_
  rw [tangentMapWithin, h p.1 hp, tangentMapWithin, mfderivWithin_congr h (h _ hp)]

Похожие утверждения