contDiffWithinAt_congr_of_mem — Mathlib

English

If f₁ agrees with f on s, then ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x.

Русский

Если f₁ совпадает с f на s, то ContDiffWithinAt 𝕜 n f₁ s x эквивалентно ContDiffWithinAt 𝕜 n f s x.

LaTeX

$$$\\forall h:\\forall y\\in s, f_1 y = f y \\Rightarrow ContDiffWithinAt 𝕜 n f_1 s x \\leftrightarrow ContDiffWithinAt 𝕜 n f s x$$$

Lean4

theorem contDiffWithinAt_congr_of_mem (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
    ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  contDiffWithinAt_congr h₁ (h₁ x hx)

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