comp_differentiable_iff — Mathlib

English

For f: G → E, s ⊆ E, x ∈ G, and iso: E ≃L[𝕜] F, HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F) ∘ f') s x is equivalent to HasFDerivWithinAt f f' s x.

Русский

Для f: G → E, s ⊆ E, x ∈ G и iso: E ≃L[𝕜] F, HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F) ∘ f') s x эквивалентно HasFDerivWithinAt f f' s x.

LaTeX

$$$HasFDerivWithinAt (iso \circ f) ((iso : E →L[𝕜] F) \circ f') s x \iff HasFDerivWithinAt f f' s x$$$

Lean4

theorem comp_differentiable_iff {f : G → E} : Differentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f :=
  by
  rw [← differentiableOn_univ, ← differentiableOn_univ]
  exact iso.comp_differentiableOn_iff

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