congr_mono — Mathlib

English

If f has MF-derivative within s at x with derivative f' and f1 equals f on t with t ⊆ s, then f1 has MF-derivative within t at x with derivative f'.

Русский

Если f имеет MF-дериватив внутри s в точке x с производной f' и f1 совпадает с f на t, причём t ⊆ s, то у f1 есть MF-дериватив внутри t в x с той же производной f'.

LaTeX

$$$HasMFDerivWithinAt\ I I'\ f\ s\ x\ f' \land (\forall y\in t, f_1(y)=f(y)) \land t\subseteq s \Rightarrow HasMFDerivWithinAt\ I I'\ f\ t\ x\ f'$$$

Lean4

theorem congr_mono (h : HasMFDerivWithinAt I I' f s x f') (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    HasMFDerivWithinAt I I' f₁ t x f' :=
  (h.mono h₁).congr_of_eventuallyEq (Filter.mem_inf_of_right ht) hx

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