extDerivWithin — Mathlib

English

If ω1 and ω2 are equal near x within s, then extDerivWithin ω1 s equals extDerivWithin ω2 s in a neighborhood of x within s.

Русский

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

LaTeX

$$$ (\\nhdsWithin x\, s).EventuallyEq\, ω_1\, ω_2 \\rightarrow (\\nhdsWithin x\, s).EventuallyEq\, (extDerivWithin(ω_1\, s))\, (extDerivWithin(ω_2\, s)) $$$

Lean4

protected theorem extDerivWithin (hs : ω₁ =ᶠ[𝓝[s] x] ω₂) : extDerivWithin ω₁ s =ᶠ[𝓝[s] x] extDerivWithin ω₂ s :=
  hs.extDerivWithin' .rfl

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