derivWithin_congr_set — Mathlib

English

For any sets s, t and data, derivWithin f (s ∩ t) x = derivWithin f s x when ht is satisfied.

Русский

Для множества s ∩ t верно derivWithin f (s ∩ t) x = derivWithin f s x при выполнении условий ht.

LaTeX

$$$$ \\ derivWithin f (s \\cap t) x = derivWithin f s x $$$$

Lean4

theorem derivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : derivWithin f s x = derivWithin f t x := by
  simp only [derivWithin, fderivWithin_congr_set h]

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