English
A function is continuous on the union of two closed sets iff it is continuous on each of them.
Русский
Функция непрерывна на объединении двух замкнутых множеств тогда и только тогда, когда она непрерывна на каждом из множеств.
LaTeX
$$$\\text{IsClosed } s \\land \\text{IsClosed } t \\Rightarrow (\\text{ContinuousOn } f (s \\cup t) \\iff (\\text{ContinuousOn } f s \\land \\text{ContinuousOn } f t))$$$
Lean4
/-- A function is continuous on two closed sets iff it is also continuous on their union. -/
theorem continouousOn_union_iff_of_isClosed {f : α → β} (hs : IsClosed s) (ht : IsClosed t) :
ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t :=
⟨fun h ↦ ⟨h.mono s.subset_union_left, h.mono s.subset_union_right⟩, fun h ↦ h.left.union_of_isClosed h.right hs ht⟩
