comp_right_differentiableAt_iff — Mathlib

English

Let iso: E ≃L[𝕜] F. Then DifferentiableAt 𝕜 (f ∘ iso) x ↔ DifferentiableAt 𝕜 f (iso x).

Русский

Пусть iso: E ≃L[𝕜] F. Тогда DifferentiableAt 𝕜 (f ∘ iso) x эквивалентно DifferentiableAt 𝕜 f (iso x).

LaTeX

$$$\DifferentiableAt 𝕜 (f \circ iso) x \iff \DifferentiableAt 𝕜 f (iso x)$$$

Lean4

theorem comp_right_differentiableAt_iff {f : F → G} {x : E} :
    DifferentiableAt 𝕜 (f ∘ iso) x ↔ DifferentiableAt 𝕜 f (iso x) := by
  simp only [← differentiableWithinAt_univ, ← iso.comp_right_differentiableWithinAt_iff, preimage_univ]

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