extDerivWithin_eq — Mathlib

English

Let ω1, ω2 be differential-like objects taking values in linear maps; if they coincide near x within s and agree at x, then their exterior derivatives within s at x agree.

Русский

Пусть ω1, ω2 — такие же дифференцируемые отображения, принимающие значения в линейных отображениях; если они совпадают в окрестности точки x внутри множества s и равны в точке x, тогда их внешние производные внутри s в точке x совпадают.

LaTeX

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

Lean4

theorem extDerivWithin_eq (hs : ω₁ =ᶠ[𝓝[s] x] ω₂) (hx : ω₁ x = ω₂ x) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x :=
  by simp only [extDerivWithin, alternatizeUncurryFin, hs.fderivWithin_eq hx]

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