contDiffWithinAt_congr_of_insert — Mathlib

English

If h1 agrees on insert x s, then ContDiffWithinAt on s for f₁ is equivalent to ContDiffWithinAt for f.

Русский

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

LaTeX

$$$\\forall h_1: \\forall y \\in \\text{insert } x s, f_1 y = f y \\Rightarrow ContDiffWithinAt 𝕜 n f_1 s x \\leftrightarrow ContDiffWithinAt 𝕜 n f s x$$$

Lean4

theorem contDiffWithinAt_congr_of_insert (h₁ : ∀ y ∈ insert x s, f₁ y = f y) :
    ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  contDiffWithinAt_congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

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