English
For a quotient map f, continuity on an open set s is equivalent to the continuity of the restricted map on the preimage.
Русский
Для квотиентного отображения f непрерывность на открытом s эквивалентна непрерывности ограниченного отображения на предобразе.
LaTeX
$$$\\text{IsQuotientMap } f \\Rightarrow \\forall s\\; \\text{IsOpen } s \\Rightarrow (\\text{ContinuousOn } f s \\iff \\text{ContinuousOn } (f|_{f^{-1}(s)}) (f^{-1}(s))$$$
Lean4
/-- If `f` is continuous on an open set `s` and continuous at each point of another
set `t` then `f` is continuous on `s ∪ t`. -/
theorem union_continuousAt {f : α → β} (s_op : IsOpen s) (hs : ContinuousOn f s) (ht : ∀ x ∈ t, ContinuousAt f x) :
ContinuousOn f (s ∪ t) :=
continuousOn_of_forall_continuousAt <| fun _ hx =>
hx.elim (fun h => ContinuousWithinAt.continuousAt (continuousWithinAt hs h) <| IsOpen.mem_nhds s_op h) (ht _)
