isSymmSndFDerivWithinAt — Mathlib

English

From a global symmetry at x, deduce the corresponding within-at symmetry on a set s containing x.

Русский

Из глобальной симметрии в точке x выводится соответствующая локальная симметрия на множествах, содержащих x.

LaTeX

$$$IsSymmSndFDerivAt 𝕜 f x \\Rightarrow IsSymmSndFDerivWithinAt 𝕜 f s x$ (при условий contdiff и уникальности)\n$$

Lean4

theorem isSymmSndFDerivWithinAt (h : IsSymmSndFDerivAt 𝕜 f x) (hf : ContDiffAt 𝕜 2 f x) (hs : UniqueDiffOn 𝕜 s)
    (hx : x ∈ s) : IsSymmSndFDerivWithinAt 𝕜 f s x :=
  by
  simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf
  exact h.mono_of_mem_nhdsWithin univ_mem hf hs uniqueDiffOn_univ hx

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