comp_contDiffOn_iff — Mathlib

English

Composition on the left by a linear equivalence preserves higher differentiability at a set point.

Русский

Композиция слева линейной эквивалентности сохраняет более высокую differentiability в точке множества.

LaTeX

$$$\forall e:\, F \simeq_{L[\mathbb{K}]} G,\; ContDiffWithinAt 𝕜 n f s x \Rightarrow ContDiffWithinAt 𝕜 n (f\circ e) s x$$$

Lean4

/-- Composition by continuous linear equivs on the left respects higher differentiability on
domains. -/
theorem comp_contDiffOn_iff (e : F ≃L[𝕜] G) : ContDiffOn 𝕜 n (e ∘ f) s ↔ ContDiffOn 𝕜 n f s := by
  simp [ContDiffOn, e.comp_contDiffWithinAt_iff]

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