contMDiffWithinAt_congr_of_mem — Mathlib

English

If f and f1 coincide on s and x ∈ s, then ContMDiffWithinAt I I' n f1 s x is equivalent to ContMDiffWithinAt I I' n f s x. The equivalence is determined by agreement on s and at x.

Русский

Если f и f1 совпадают на s и x ∈ s, то ContMDiffWithinAt I I' n f1 s x эквивалентно ContMDiffWithinAt I I' n f s x. Эквивалентность определяется согласованием на s и в x.

LaTeX

$$$(\forall y \in s, f_1 y = f y) \land x \in s \Rightarrow ContMDiffWithinAt I I' n f_1 s x \Leftrightarrow ContMDiffWithinAt I I' n f s x.$$$

Lean4

theorem contMDiffWithinAt_congr_of_mem (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
    ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_mem h₁ hx

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