hasLineDerivWithinAt_congr_set — Mathlib

English

Equivalent formulation for congruence under nhds equivalence of sets on line derivatives.

Русский

Эквивалентная формулировка конгруэнтности для линейной производной вдоль линии при эквивалентности множеств во множестве окрестности.

LaTeX

$$$HasLineDerivWithinAt_{\mathbb{k}}(f,f',s,x,v) \iff HasLineDerivWithinAt_{\mathbb{k}}(f,f',t,x,v)$ при $s =_\mathcal{N} t$$$

Lean4

theorem hasLineDerivWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
    HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v :=
  by
  apply hasDerivWithinAt_congr_set
  let F := fun (t : 𝕜) ↦ x + t • v
  have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
  have : s =ᶠ[𝓝 (F 0)] t := by convert h; simp [F]
  exact B.preimage_mem_nhds this

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