mono_of_mem_nhdsWithin — Mathlib

English

A variant form asserting the same congruence property for HasLineDerivWithinAt under nhds equivalence of sets.

Русский

Вариант утверждения той же самой конгруэнтности для HasLineDerivWithinAt при эквивалентности множеств в nhds.

LaTeX

$$$ (nhds x).EventuallyEq s t \Rightarrow HasLineDerivWithinAt_{\mathbb{k}}(f,f',s,x,v) \iff HasLineDerivWithinAt_{\mathbb{k}}(f,f',t,x,v) $$$

Lean4

theorem mono_of_mem_nhdsWithin (h : HasLineDerivWithinAt 𝕜 f f' t x v) (hst : t ∈ 𝓝[s] x) :
    HasLineDerivWithinAt 𝕜 f f' s x v :=
  by
  apply HasDerivWithinAt.mono_of_mem_nhdsWithin h
  apply ContinuousWithinAt.preimage_mem_nhdsWithin'' _ hst (by simp)
  apply Continuous.continuousWithinAt; fun_prop

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