Continuity from a cover by two closed sets #
A map that is continuous within each of two closed sets covering the space, at those of them
that contain a point, is continuous at that point: continuity within a closed set not containing
the point holds vacuously. 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 derivative counterpart is TauCeti.hasFDerivAt_of_isClosed_of_union_eq_univ.
theorem
TauCeti.continuousAt_of_isClosed_of_union_eq_univ
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s t : Set X}
{x : X}
(hs : IsClosed s)
(ht : IsClosed t)
(hst : s ∪ t = Set.univ)
(h₁ : x ∈ s → ContinuousWithinAt f s x)
(h₂ : x ∈ t → ContinuousWithinAt f t x)
:
ContinuousAt f x
A map continuous within each of two closed sets covering the space, at those of them that
contain x, is continuous at x.