derivWithin_congr_set' — Mathlib

English

The derivative within the universal set equals the usual derivative: derivWithin f univ = deriv f.

Русский

Производная внутри множества унив равна обычной производной: derivWithin f univ = deriv f.

LaTeX

$$$$ \\ derivWithin f univ = deriv f $$$$

Lean4

theorem derivWithin_congr_set' (y : 𝕜) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) : derivWithin f s x = derivWithin f t x := by
  simp only [derivWithin, fderivWithin_congr_set' y h]

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