tangentMapWithin_eq_tangentMap — Mathlib

English

If two conditions give the same tangent map, then tangent maps within s and within p coincide.

Русский

Если две предпосылки дают одинаковую касательную карту, то касательные карты внутри s и внутри p совпадают.

LaTeX

$$$$tangentMapWithin I I' f s p = tangentMapWithin I I' f t p \\text{ under appropriate hypotheses}$$$$

Lean4

theorem tangentMapWithin_eq_tangentMap {p : TangentBundle I M} (hs : UniqueMDiffWithinAt I s p.1)
    (h : MDifferentiableAt I I' f p.1) : tangentMapWithin I I' f s p = tangentMap I I' f p :=
  by
  rw [← mdifferentiableWithinAt_univ] at h
  rw [← tangentMapWithin_univ]
  exact tangentMapWithin_subset (subset_univ _) hs h

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