congr_mono — Mathlib

English

If f and f₁ agree on s and x, then the line-derivative within s is the same as the line-derivative within s for f₁.

Русский

Если f и f₁ совпадают на s и в x, то линейная производная внутри s совпадает между ними.

LaTeX

$$$\text{EqOn}(f_1,f,s) \Rightarrow \text{Eq}(\text{lineDerivWithin}_{\mathbb{k}}(f_1,s,x,v), \text{lineDerivWithin}_{\mathbb{k}}(f,s,x,v))$$$

Lean4

theorem congr_mono (h : LineDifferentiableWithinAt 𝕜 f s x v) (ht : EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    LineDifferentiableWithinAt 𝕜 f₁ t x v :=
  (HasLineDerivWithinAt.congr_mono h.hasLineDerivWithinAt ht hx h₁).differentiableWithinAt

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