extDerivWithin_eq_of_insert — Mathlib

English

If ω1 and ω2 are eventually equal around x with respect to the nhds of the point x taken at insert x s, then extDerivWithin ω1 s x = extDerivWithin ω2 s x.

Русский

Если ω1 и ω2 совпадают около точки x в окрестности, взятой по добавлению точки x в s, то extDerivWithin ω1 s x = extDerivWithin ω2 s x.

LaTeX

$$$ (\\nhdsWithin x \\,(\\operatorname{insert} x\, s)).EventuallyEq\, ω_1\, ω_2 \\rightarrow extDerivWithin(ω_1\, s\, x) = extDerivWithin(ω_2\, s\, x) $$$

Lean4

theorem extDerivWithin_eq_of_insert (hs : ω₁ =ᶠ[𝓝[insert x s] x] ω₂) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x :=
  by
  apply Filter.EventuallyEq.extDerivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)
  exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

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