comp_contDiff_iff — Mathlib

English

If e is a continuous linear equivalence, then ContDiff 𝕜 n f x is equivalent to ContDiff 𝕜 n (f ∘ e) at the corresponding point.

Русский

Если e линейная эквивалентность, тогда дифференцируемость f и f∘e равны в точке.

LaTeX

$$$\text{ContDiff}_{\mathbb{K}}^n f x \Leftrightarrow \text{ContDiff}_{\mathbb{K}}^n (f\circ e) (e^{-1}x) $$$

Lean4

/-- Composition by continuous linear equivs on the left respects higher differentiability. -/
theorem comp_contDiff_iff (e : F ≃L[𝕜] G) : ContDiff 𝕜 n (e ∘ f) ↔ ContDiff 𝕜 n f := by
  simp only [← contDiffOn_univ, e.comp_contDiffOn_iff]

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