contDiffWithinAt_congr — Mathlib

English

If f and f1 agree on s and x ∈ s, then ContDiffWithinAt is preserved from f to f1.

Русский

Если f и f1 совпадают на s и x принадлежит s, ContDiffWithinAt сохраняется при переходе от f к f1.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \\Rightarrow (∀ y∈s, f1 y = f y) \\Rightarrow x ∈ s \\Rightarrow ContDiffWithinAt 𝕜 n f1 s x$$

Lean4

theorem contDiffWithinAt_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
    ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  ⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦ h'.congr h₁ hx⟩

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