contMDiffWithinAt_insert_self — Mathlib

English

Inserting the point x into the set does not change the ContMDiffWithinAt property at x.

Русский

Добавление точки x в множество не меняет свойство ContMDiffWithinAt в точке x.

LaTeX

$$$ ContMDiffWithinAt I I' n f (insert x s) x \iff ContMDiffWithinAt I I' n f s x $$$

Lean4

theorem contMDiffWithinAt_insert_self : ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x :=
  by
  simp only [contMDiffWithinAt_iff, continuousWithinAt_insert_self]
  refine Iff.rfl.and <| (contDiffWithinAt_congr_set ?_).trans contDiffWithinAt_insert_self
  simp only [← map_extChartAt_nhdsWithin, nhdsWithin_insert, Filter.map_sup, Filter.map_pure,
    ← nhdsWithin_eq_iff_eventuallyEq]

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