extDerivWithin_congr' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem extDerivWithin_congr' (hs : EqOn ω₁ ω₂ s) (hx : x ∈ s) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x :=
  extDerivWithin_congr hs (hs hx)

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