sumCongr — Mathlib

English

Sum of two homeomorphisms gives a homeomorphism on sums.

Русский

Сумма двух гомеоморфизмов задаёт гомеоморфизм над суммами.

LaTeX

$$$$\\mathrm{Homeomorph}(X ⊕ Y, X' ⊕ Y') \\text{ from } h_1,h_2 \\text{ where } h_1:X≃ₜX', h_2:Y≃ₜY'.$$$$

Lean4

/-- Sum of two homeomorphisms. -/
def sumCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X ⊕ Y ≃ₜ X' ⊕ Y'
    where
  continuous_toFun := h₁.continuous.sumMap h₂.continuous
  continuous_invFun := h₁.symm.continuous.sumMap h₂.symm.continuous
  toEquiv := h₁.toEquiv.sumCongr h₂.toEquiv

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