English
Let X, Y, Z be topological spaces. A map f: X ⊕ Y → Z is continuous if and only if its compositions with the left and right inclusions are continuous.
Русский
Пусть X, Y, Z — топологические пространства. Функция f: X ⊕ Y → Z непрерывна тогда и только тогда, когда композиции f ∘ inl и f ∘ inr непрерывны.
LaTeX
$$$\\\\operatorname{Continuous}(f) \\\\iff \\\\operatorname{Continuous}(f \\\\circ \\\\mathrm{inl}) \land \\\\operatorname{Continuous}(f \\\\circ \\\\mathrm{inr}).$$$
Lean4
theorem continuous_sum_dom {f : X ⊕ Y → Z} : Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr) :=
(continuous_sup_dom (t₁ := TopologicalSpace.coinduced Sum.inl _) (t₂ :=
TopologicalSpace.coinduced Sum.inr _)).trans <|
continuous_coinduced_dom.and continuous_coinduced_dom
