prodCongr — Mathlib

English

If h1: X ≃ₜ X' and h2: Y ≃ₜ Y', then there is a natural homeomorphism X × Y ≃ₜ X' × Y' given by h1.prodCongr h2.

Русский

Если существуют гомеоморфизмы h1: X ≃ₜ X' и h2: Y ≃ₜ Y', то существует естественный гомеоморфизм X × Y ≃ₜ X' × Y' заданный через h1.prodCongr h2.

LaTeX

$$$(h_1 : X \simeq_t X') \land (h_2 : Y \simeq_t Y') \Rightarrow (h_1.prodCongr h_2) : X \times Y \simeq_t X' \times Y'$$$

Lean4

/-- Product of two homeomorphisms. -/
def prodCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X × Y ≃ₜ X' × Y'
    where
  toEquiv := h₁.toEquiv.prodCongr h₂.toEquiv
  continuous_toFun := by dsimp; fun_prop
  continuous_invFun := by dsimp; fun_prop

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