extDerivWithin_congr — Mathlib

English

If ω1 and ω2 coincide on s and ω1 x = ω2 x, then extDerivWithin ω1 s x = extDerivWithin ω2 s x.

Русский

Если ω1 и ω2 совпадают на s и ω1 x = ω2 x, то extDerivWithin ω1 s x = extDerivWithin ω2 s x.

LaTeX

$$$ hs : EqOn(ω_1, ω_2, s) \\rightarrow hx : ω_1 x = ω_2 x \\rightarrow extDerivWithin(ω_1\, s\, x) = extDerivWithin(ω_2\, s\, x) $$$

Lean4

theorem extDerivWithin_congr (hs : EqOn ω₁ ω₂ s) (hx : ω₁ x = ω₂ x) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x :=
  (hs.eventuallyEq.filter_mono inf_le_right).extDerivWithin_eq hx

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