extDerivWithin' — Mathlib

English

If ω1 and ω2 coincide near x within s, then the restricted derivatives on any t ⊆ s are eventually equal near x with respect to s.

Русский

Если ω1 и ω2 совпадают около x внутри s, то производные на любом подмножестве t ⊆ s совпадут в нужной предельной концепции.

LaTeX

$$$ (\\omega_1 =^\\mathrm{nhdsWithin}_{s} \\, ω_2) \\rightarrow (t \\subseteq s) \\rightarrow extDerivWithin(ω_1\, t) =^\\mathrm{nhdsWithin}_{s} extDerivWithin(ω_2\, t) $$$

Lean4

theorem extDerivWithin' (hs : ω₁ =ᶠ[𝓝[s] x] ω₂) (ht : t ⊆ s) : extDerivWithin ω₁ t =ᶠ[𝓝[s] x] extDerivWithin ω₂ t :=
  (eventually_eventually_nhdsWithin.2 hs).mp <|
    eventually_mem_nhdsWithin.mono fun _y hys hs =>
      EventuallyEq.extDerivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht) (hs.self_of_nhdsWithin hys)

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