English
A function is continuous on the union of open sets if and only if it is continuous on each of the sets.
Русский
Функция непрерывна на объединении открытых множеств тогда и только тогда, когда она непрерывна на каждом из множеств.
LaTeX
$$$\\text{IsOpen } s \\land \\text{IsOpen } 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 open sets iff it is also continuous on their union. -/
theorem continouousOn_union_iff_of_isOpen {f : α → β} (hs : IsOpen s) (ht : IsOpen 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_isOpen h.right hs ht⟩
