trans_toHomotopyEquiv — Mathlib

English

The homotopy equivalence associated to the composition of two homeomorphisms equals the composition of the associated homotopy equivalences.

Русский

Гомотопическая эквивалентность композиции двух гомеоморфизмов равна композиции соответствующих гомотопических эквивалентностей.

LaTeX

$$$(h_0: X\simeq_t Y)\; (h_1: Y\simeq_t Z) \Rightarrow (h_0.trans h_1).toHomotopyEquiv = h_0.toHomotopyEquiv.trans h_1.toHomotopyEquiv$$$

Lean4

@[simp]
theorem trans_toHomotopyEquiv (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :
    (h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv :=
  rfl

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