hasMFDerivWithinAt_diff_singleton

English

Inserting a point into the domain preserves the HasMFDerivWithinAt property.

Русский

Вставка точки в область определения сохраняет свойство HasMFDerivWithinAt.

LaTeX

$$$ (h : HasMFDerivWithinAt I I' f s x f') \Rightarrow HasMFDerivWithinAt I I' f (Set.insert y s) x f' $$$

Lean4

theorem hasMFDerivWithinAt_diff_singleton (y : M) :
    HasMFDerivWithinAt I I' f (s \ { y }) x f' ↔ HasMFDerivWithinAt I I' f s x f' := by
  rw [← hasMFDerivWithinAt_insert, insert_diff_singleton, hasMFDerivWithinAt_insert]

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