contDiffWithinAt_congr_set — Mathlib

English

If h1 holds for insert x s, then ContDiffWithinAt 𝕜 n f1 s x iff ContDiffWithinAt 𝕜 n f s x.

Русский

Если h1 верна для insert x s, то ContDiffWithinAt 𝕜 n f1 s x эквивалентно ContDiffWithinAt 𝕜 n f s x.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f1 s x \\iff ContDiffWithinAt 𝕜 n f s x$$

Lean4

theorem contDiffWithinAt_congr_set {t : Set E} (hst : s =ᶠ[𝓝 x] t) :
    ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n f t x :=
  ⟨fun h => h.congr_set hst, fun h => h.congr_set hst.symm⟩

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