contDiffOn_pi — Mathlib

English

simp lemma for Pi' version of HasFTaylorSeriesUpToOn: HasFTaylorSeriesUpToOn n Φ P' s is equivalent to the given Pi' expression for all i.

Русский

Лемма упрощения для версии Pi' HasFTaylorSeriesUpToOn: эквивалентно выражению для всех i.

LaTeX

$$$ HasFTaylorSeriesUpToOn n Φ P' s \iff \forall i, HasFTaylorSeriesUpToOn n (\\lambda x. Φ x i) (\\lambda x m. (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap (P' x m)) s $$$

Lean4

theorem contDiffOn_pi : ContDiffOn 𝕜 n Φ s ↔ ∀ i, ContDiffOn 𝕜 n (fun x => Φ x i) s :=
  ⟨fun h _ x hx => contDiffWithinAt_pi.1 (h x hx) _, fun h x hx => contDiffWithinAt_pi.2 fun i => h i x hx⟩

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