continuous_sumMap — Mathlib

English

Let f: X → Y and g: Z → W be maps. The combined map Sum.map f g is continuous if and only if f and g are continuous.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem continuous_sumMap {f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g :=
  continuous_sumElim.trans <| IsEmbedding.inl.continuous_iff.symm.and IsEmbedding.inr.continuous_iff.symm

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