congr — Mathlib

English

If hf is ContMDiffOn on s and f1 agrees with f on s1 ⊆ s, then f1 is ContMDiffOn on s1.

Русский

Если hf = ContMDiffOn на s и f1 совпадает с f на подмножество s1 ⊆ s, то f1 ∈ ContMDiffOn на s1.

LaTeX

$$$ hf : ContMDiffOn I I' n f s \to \; h1 : \forall y \in s1, f1 y = f y \to ContMDiffOn I I' n f1 s1$$

Lean4

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

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