mfderivWithin_congr_of_mem — Mathlib

English

If two maps agree on a set s in a neighborhood of x, then their tangent map within s at x agree on p.

Русский

Если две отображения совпадают на области s в окрестности x, то их тангенциальные отображения внутри s в точке p совпадают.

LaTeX

$$$\\forall p\\in \\text{TangentBundle},\\; (f|_{s}=f_1|_{s})\\Rightarrow tangentMapWithin I I' f\\,s\\,p = tangentMapWithin I I' f_1\\,s\\,p$$$

Lean4

theorem mfderivWithin_congr_of_mem (hL : ∀ x ∈ s, f₁ x = f x) (hx : x ∈ s) :
    mfderivWithin I I' f₁ s x = mfderivWithin I I' f s x :=
  Filter.EventuallyEq.mfderivWithin_eq_of_mem (Filter.eventuallyEq_of_mem self_mem_nhdsWithin hL) hx

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