congr_mono — Mathlib

English

If HasGradientWithinAt f f' s x holds and f₁ equals f on s, then HasGradientWithinAt f₁ f' s x.

Русский

Если функция имеет градиент внутри множества s в точке x, и другая функция совпадает с ней на s, то обладаёт тем же градиентом внутри s в x.

LaTeX

$$HasGradientWithinAt f f' s x → (∀ x ∈ s, f₁ x = f x) → HasGradientWithinAt f₁ f' s x$$

Lean4

theorem congr_mono (h : HasGradientWithinAt f f' s x) (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    HasGradientWithinAt f₁ f' t x :=
  HasFDerivWithinAt.congr_mono h ht hx h₁

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