trans — Mathlib

English

Composition of two homeomorphisms is a homeomorphism.

Русский

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

LaTeX

$$$$ h_1: X \simeq_t Y,\; h_2: Y \simeq_t Z \;\Rightarrow\; h_1 \text{ trans } h_2 : X \simeq_t Z. $$$$

Lean4

/-- Composition of two homeomorphisms. -/
@[trans]
protected def trans (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z
    where
  continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun
  continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun
  toEquiv := Equiv.trans h₁.toEquiv h₂.toEquiv

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