sumMap — Mathlib

English

If f and g are homeomorphisms, then their sum map (acting componentwise on a coproduct) is a homeomorphism.

Русский

Если f и g — гомеоморфизмы, то их сумма (поэлементное отображение на сумме) является гомеоморфизмом.

LaTeX

$$$\IsHomeomorph f \to \IsHomeomorph g \to IsHomeomorph(\mathrm{Sum.map}(f,g))$$$

Lean4

theorem sumMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Sum.map f g) :=
  ⟨hf.1.sumMap hg.1, hf.2.sumMap hg.2, hf.3.sumMap hg.3⟩

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