congr — Mathlib

English

If f1 equals f on s, then differentiability on s for f1 is equivalent to differentiability on s for f.

Русский

Если f1 совпадает с f на s, то дифференцируемость на s для f1 равна дифференцируемости на s для f.

LaTeX

$$$MDifferentiableOn I I' f_1 s \iff MDifferentiableOn I I' f s$$$

Lean4

theorem congr (h : MDifferentiableOn I I' f s) (h₁ : ∀ y ∈ s, f₁ y = f y) : MDifferentiableOn I I' f₁ s :=
  differentiableWithinAt_localInvariantProp.liftPropOn_congr h h₁

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