congr_mono — Mathlib

English

If h gives a line derivative for f along s, and f agrees with f₁ on t, with t ⊆ s and f₁ x = f x, then f₁ has the same line derivative on t.

Русский

Если имеется линейная производная для f вдоль s, и f совпадает с f₁ на t, причём t ⊆ s и f₁(x) = f(x), то в точке x вдоль t линейная производная у f₁ совпадает с у f.

LaTeX

$$$\text{HasLineDerivWithinAt}_{\mathbb{k}}(f,f',s,x,v) \Rightarrow (t\subseteq s) \rightarrow (f=f on t) \rightarrow \text{HasLineDerivWithinAt}_{\mathbb{k}}(f_1,f',t,x,v)$$$

Lean4

theorem congr_mono (h : HasLineDerivWithinAt 𝕜 f f' s x v) (ht : EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    HasLineDerivWithinAt 𝕜 f₁ f' t x v :=
  HasDerivWithinAt.congr_mono h (fun _ hy ↦ ht hy) (by simpa using hx) (preimage_mono h₁)

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