Derivatives from a cover by two closed sets #
A map that has the same derivative within each of two closed sets covering the space, at those
of them that contain a point, has that derivative at the point: a derivative within a closed set
not containing the point holds vacuously, and Mathlib's HasFDerivWithinAt.union combines the
two pieces. This glues maps defined by cases on closed pieces, such as the two closed half-planes
on either side of a line (TauCeti.Analysis.Complex.EvenReflection).
The continuity counterpart is TauCeti.continuousAt_of_isClosed_of_union_eq_univ.
theorem
TauCeti.hasFDerivAt_of_isClosed_of_union_eq_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' : E →L[𝕜] F}
{s t : Set E}
{x : E}
(hs : IsClosed s)
(ht : IsClosed t)
(hst : s ∪ t = Set.univ)
(h₁ : x ∈ s → HasFDerivWithinAt f f' s x)
(h₂ : x ∈ t → HasFDerivWithinAt f f' t x)
:
HasFDerivAt f f' x
A map with derivative f' within each of two closed sets covering the space, at those of
them that contain x, has derivative f' at x.