contDiff_comp_iff — Mathlib

English

Let e be a continuous linear equivalence e : G ≃L[𝕜] E. Then for any f : E → F, ContDiff 𝕜 n (f ∘ e) holds if and only if ContDiff 𝕜 n f holds.

Русский

Пусть e — непрерывное линейное эквивалентное отображение G в E. Тогда для любой f: E → F выполняется ContDiff 𝕜 n (f ∘ e) ⇔ ContDiff 𝕜 n f.

LaTeX

$$$ \operatorname{ContDiff}_{\mathbb{K}}^{n} (f \circ e) \Longleftrightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} f $$$

Lean4

/-- Composition by continuous linear equivs on the right respects higher differentiability. -/
theorem contDiff_comp_iff (e : G ≃L[𝕜] E) : ContDiff 𝕜 n (f ∘ e) ↔ ContDiff 𝕜 n f :=
  by
  rw [← contDiffOn_univ, ← contDiffOn_univ, ← preimage_univ]
  exact e.contDiffOn_comp_iff

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