comp_differentiableWithinAt_iff — Mathlib

English

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

Русский

Для iso: E ≃L[𝕜] F и любого f: G → E, DifferentiableWithinAt 𝕜 (iso ∘ f) s x эквивалентно DifferentiableWithinAt 𝕜 f s x.

LaTeX

$$$\DifferentiableWithinAt 𝕜 (iso \circ f) s x \;\Longleftrightarrow\; \DifferentiableWithinAt 𝕜 f s x$$$

Lean4

theorem comp_differentiableWithinAt_iff {f : G → E} {s : Set G} {x : G} :
    DifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  by
  refine ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
  have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
    iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H
  rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

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