trans — Mathlib

English

If X ≃ₕ Y and Y ≃ₕ Z, then X ≃ₕ Z.

Русский

Если X ≃ₕ Y и Y ≃ₕ Z, тогда X ≃ₕ Z.

LaTeX

$$$(X\simeq_h Y) \land (Y\simeq_h Z) \Rightarrow (X\simeq_h Z)$$$

Lean4

/-- If `X` is homotopy equivalent to `Y`, and `Y` is homotopy equivalent to `Z`, then `X` is homotopy
equivalent to `Z`.
-/
@[simps!]
def trans (h₁ : X ≃ₕ Y) (h₂ : Y ≃ₕ Z) : X ≃ₕ Z
    where
  toFun := h₂.toFun.comp h₁.toFun
  invFun := h₁.invFun.comp h₂.invFun
  left_inv := by
    refine Homotopic.trans ?_ h₁.left_inv
    exact .comp (.refl _) (.comp h₂.left_inv (.refl _))
  right_inv := by
    refine Homotopic.trans ?_ h₂.right_inv
    exact .comp (.refl _) <| .comp h₁.right_inv (.refl _)

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