instIsMultiplicativeQuasiIso — Mathlib

English

For a homotopy equivalence e: K ≃ H L, the homotopy map e.hom is a quasi-isomorphism at every i.

Русский

Для гомотопического эквивалента e: K ≃ L отображение e.hom является квазиизоморфизмом на каждом i.

LaTeX

$$$\forall i,\ QI_i(e.hom).$$$

Lean4

instance : (quasiIso C c).IsMultiplicative
    where
  id_mem
    _ := by
    rw [mem_quasiIso_iff]
    infer_instance
  comp_mem _ _ hf
    hg := by
    rw [mem_quasiIso_iff] at hf hg ⊢
    infer_instance

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