extDeriv_eq

Mathlib.Analysis.Calculus.DifferentialForm.Basic

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyEq.extDeriv_eq

English

If ω1 and ω2 are nhds-equivalent at x, then extDeriv ω1 x = extDeriv ω2 x.

Русский

Если ω1 и ω2 эквивалентны по мере близости к x, тоextDeriv ω1 x = extDeriv ω2 x.

LaTeX

$$$ (\\nhds x).EventuallyEq\\, ω_1\\, ω_2 \\rightarrow extDeriv(ω_1\, x) = extDeriv(ω_2\, x) $$$

Lean4

theorem extDeriv_eq (h : ω₁ =ᶠ[𝓝 x] ω₂) : extDeriv ω₁ x = extDeriv ω₂ x :=
  h.extDeriv.self_of_nhds

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru