continuous_sumElim — Mathlib

English

Let f: X → Z and g: Y → Z. The map Sum.elim f g: X ⊕ Y → Z is continuous iff f and g are continuous.

Русский

Пусть f: X → Z и g: Y → Z. Отображение Sum.elim f g: X ⊕ Y → Z непрерывно тогда и только тогда, когда f и g непрерывны.

LaTeX

$$$\\\\operatorname{Continuous}(\\\\mathrm{Sum.elim}(f,g)) \\\\iff \\\\operatorname{Continuous}(f) \land \\\\operatorname{Continuous}(g).$$$

Lean4

theorem continuous_sumElim {f : X → Z} {g : Y → Z} : Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g :=
  continuous_sum_dom

Похожие утверждения