ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<GOAL>DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<GOAL>DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<GOAL>Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasStrictFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasStrictFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] F<GOAL>HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm).comp f') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] F<GOAL>HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f ((↑iso.symm).comp f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑iso ∘ f) s x = (↑iso).comp (fderivWithin 𝕜 f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>fderiv 𝕜 (⇑iso ∘ f) x = (↑iso).comp (fderiv 𝕜 f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>x : E<VAR>s : Set E<VAR>L : G ≃L[𝕜] G'<VAR>f : E → F →L[𝕜] G<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => (↑L).comp (f x)) s x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderivWithin 𝕜 f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>L : G ≃L[𝕜] G'<VAR>f : E → F →L[𝕜] G<VAR>x : E<GOAL>fderiv 𝕜 (fun x => (↑L).comp (f x)) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>L : G ≃L[𝕜] G'<VAR>f : E → F →L[𝕜] G<GOAL>(fderiv 𝕜 fun x => (↑L).comp (f x)) = fun x => (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<GOAL>DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<GOAL>DifferentiableAt 𝕜 (f ∘ ⇑iso) x ↔ DifferentiableAt 𝕜 f (iso x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<GOAL>DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<GOAL>Differentiable 𝕜 (f ∘ ⇑iso) ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<GOAL>HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<VAR>f' : F →L[𝕜] G<GOAL>HasFDerivAt (f ∘ ⇑iso) (f'.comp ↑iso) x ↔ HasFDerivAt f f' (iso x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : E →L[𝕜] G<GOAL>HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f'.comp ↑iso.symm) s (iso x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<VAR>f' : E →L[𝕜] G<GOAL>HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f'.comp ↑iso.symm) (iso x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x<GOAL>fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = (fderivWithin 𝕜 f s (iso x)).comp ↑iso
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<GOAL>fderiv 𝕜 (f ∘ ⇑iso) x = (fderiv 𝕜 f (iso x)).comp ↑iso
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>HasStrictFDerivAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>HasFDerivWithinAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>HasFDerivAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>DifferentiableAt 𝕜 (⇑iso) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>DifferentiableWithinAt 𝕜 (⇑iso) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>fderiv 𝕜 (⇑iso) x = ↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑iso) s x = ↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>Differentiable 𝕜 ⇑iso
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>iso : E ≃ₗᵢ[𝕜] F<GOAL>DifferentiableOn 𝕜 (⇑iso) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<GOAL>DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>s : Set G<GOAL>DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<GOAL>Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasFDerivWithinAt (⇑iso ∘ f) ((↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') s x ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasStrictFDerivAt (⇑iso ∘ f) ((↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') x ↔ HasStrictFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasFDerivAt (⇑iso ∘ f) ((↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') x ↔ HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] F<GOAL>HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑{ toLinearEquiv := iso.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] F<GOAL>HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f ((↑{ toLinearEquiv := iso.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑iso ∘ f) s x = (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderivWithin 𝕜 f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>fderiv 𝕜 (⇑iso ∘ f) x = (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<GOAL>fderiv 𝕜 (⇑iso ∘ f) = fun x => (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>HasStrictFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>HasFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>f' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>htff' : HasStrictFDerivAt (↑f) (↑f') (↑f.symm a)<GOAL>HasStrictFDerivAt (↑f.symm) (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>f' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>htff' : HasFDerivAt (↑f) (↑f') (↑f.symm a)<GOAL>HasFDerivAt (↑f.symm) (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<GOAL>∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<GOAL>∀ᶠ (z : E) in 𝓝[≠] x, f z ≠ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>L : Filter E<GOAL>Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>v : E<GOAL>Filter.Tendsto (fun c => c • (f (x + c⁻¹ • v) - f x)) Filter.atTop (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<GOAL>Set.MapsTo (⇑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h' : DenseRange ⇑f'<GOAL>UniqueDiffWithinAt 𝕜 (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[𝕜] F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hd : ∀ x ∈ s, DenseRange ⇑(f' x)<GOAL>UniqueDiffOn 𝕜 (f '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>e' : E ≃L[𝕜] F<VAR>h : HasFDerivWithinAt f (↑e') s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>UniqueDiffWithinAt 𝕜 (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>e : E ≃L[𝕜] F<VAR>h : UniqueDiffOn 𝕜 s<GOAL>UniqueDiffOn 𝕜 (⇑e '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>e : E ≃L[𝕜] F<GOAL>UniqueDiffOn 𝕜 (⇑e '' s) ↔ UniqueDiffOn 𝕜 s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>e : F ≃L[𝕜] E<GOAL>UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
<GOAL>UpperHalfPlane.atImInfty.HasBasis (fun x => True) fun i => UpperHalfPlane.im ⁻¹' Set.Ici i
<VAR>S : Set ℍ<GOAL>S ∈ UpperHalfPlane.atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S
<VAR>α : Type u_1<VAR>NormedField α<GOAL>UpperHalfPlane.IsBoundedAtImInfty 0
<VAR>f g : ℍ → ℂ<VAR>hf : UpperHalfPlane.IsBoundedAtImInfty f<VAR>hg : UpperHalfPlane.IsBoundedAtImInfty g<GOAL>UpperHalfPlane.IsBoundedAtImInfty (f * g)
<VAR>f : ℍ → ℂ<GOAL>UpperHalfPlane.IsBoundedAtImInfty f ↔ ∃ M A, ∀ (z : ℍ), A ≤ z.im → Complex.abs (f z) ≤ M
<VAR>f : ℍ → ℂ<GOAL>UpperHalfPlane.IsZeroAtImInfty f ↔ ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ z.im → Complex.abs (f z) ≤ ε
<VAR>A B : ℝ<VAR>z : ℍ<GOAL>z ∈ UpperHalfPlane.verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im
<VAR>A B A' B' : ℝ<VAR>hA : A ≤ A'<VAR>hB : B' ≤ B<GOAL>UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B'
<VAR>A A' : ℝ<VAR>h : A ≤ A'<VAR>B : ℝ<GOAL>UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B
<VAR>A : ℝ<VAR>B B' : ℝ<VAR>h : B' ≤ B<GOAL>UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A B'
<VAR>K : Set ℍ<VAR>hK : IsCompact K<GOAL>∃ A B, 0 < B ∧ K ⊆ UpperHalfPlane.verticalStrip A B
<VAR>z : ℍ<VAR>N : ℕ<VAR>hn : 0 < N<GOAL>∃ n, ModularGroup.T ^ (↑N * n) • z ∈ UpperHalfPlane.verticalStrip (↑N) z.im
<VAR>z : ℍ<GOAL>↑UpperHalfPlane.ofComplex ↑z = z
<VAR>f : ℍ → ℂ<VAR>z : ℍ<GOAL>(f ∘ ↑UpperHalfPlane.ofComplex) ↑z = f z
<VAR>a : ↥circle<VAR>z : ℂ<GOAL>(rotation a) z = ↑a * z
<VAR>a : ↥circle<GOAL>(rotation a).symm = rotation a⁻¹
<VAR>a b : ↥circle<GOAL>(rotation a).trans (rotation b) = rotation (b * a)
<VAR>a : ↥circle<GOAL>rotation a ≠ Complex.conjLIE
<VAR>e : ℂ ≃ₗᵢ[ℝ] ℂ<GOAL>↑(rotationOf e) = e 1 / ↑(Complex.abs (e 1))
<VAR>a : ↥circle<GOAL>rotationOf (rotation a) = a
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<GOAL>f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = Complex.conjLIE
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<GOAL>∃ a, f = rotation a ∨ f = Complex.conjLIE.trans (rotation a)
<VAR>a : ↥circle<GOAL>(LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) ↑(rotation a).toLinearEquiv = ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯)
<VAR>a : ↥circle<GOAL>LinearMap.det ↑(rotation a).toLinearEquiv = 1
<VAR>z : Complex.UnitDisc<GOAL>Complex.abs ↑z < 1
<VAR>z : Complex.UnitDisc<GOAL>Complex.abs ↑z ≠ 1
<VAR>z : Complex.UnitDisc<GOAL>Complex.normSq ↑z < 1
<VAR>z : Complex.UnitDisc<GOAL>↑z ≠ 1
<VAR>z : Complex.UnitDisc<GOAL>↑z ≠ -1
<VAR>z : Complex.UnitDisc<GOAL>1 + ↑z ≠ 0
<VAR>z w : Complex.UnitDisc<GOAL>↑(z * w) = ↑z * ↑w
<VAR>z : ℂ<VAR>hz : Complex.abs z < 1<GOAL>↑(Complex.UnitDisc.mk z hz) = z
<VAR>z : Complex.UnitDisc<VAR>hz : Complex.abs ↑z < 1 := ⋯<GOAL>Complex.UnitDisc.mk (↑z) hz = z