mono_of_mem_nhdsWithin — Mathlib

English

If a symmetry property holds on t and t is nhdsWithin of s at x, then it holds on s at x as well.

Русский

Если условие сохраняется на t и t внутри nhdsWithin s в x, то оно сохраняется и на s в x.

LaTeX

$$$h : IsSymmSndFDerivWithinAt 𝕜 f t x \\Rightarrow t \\in 𝓝[s] x \\Rightarrow ContDiffWithinAt 𝕜 2 f t x \\Rightarrow UniqueDiffOn 𝕜 s \\Rightarrow UniqueDiffOn 𝕜 t \\Rightarrow x \\in s \\Rightarrow IsSymmSndFDerivWithinAt 𝕜 f s x$$$

Lean4

theorem mono_of_mem_nhdsWithin (h : IsSymmSndFDerivWithinAt 𝕜 f t x) (hst : t ∈ 𝓝[s] x)
    (hf : ContDiffWithinAt 𝕜 2 f t x) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hx : x ∈ s) :
    IsSymmSndFDerivWithinAt 𝕜 f s x := by
  intro v w
  rw [fderivWithin_fderivWithin_eq_of_mem_nhdsWithin hst hf hs ht hx]
  exact h v w

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