quasiIso_iff_comp_right — Mathlib

English

Let φ: S1 → S2 and φ′: S2 → S3 with φ′ a quasi-isomorphism. Then φ ≫ φ′ is a quasi-isomorphism if and only if φ is a quasi-isomorphism.

Русский

Пусть φ: S1 → S2 и φ′: S2 → S3 и φ′ — квазиизоморфизм. Тогда φ ≫ φ′ — квазиизоморфизм тогда и только тогда, когда φ — квазиизоморфизм.

LaTeX

$$$\operatorname{QuasiIso}(\varphi \circ \varphi') \iff \operatorname{QuasiIso}(\varphi)$ (при условии $\operatorname{QuasiIso}(\varphi')$)$$

Lean4

theorem quasiIso_iff_comp_right (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : QuasiIso φ'] : QuasiIso (φ ≫ φ') ↔ QuasiIso φ :=
  by
  constructor
  · intro
    exact quasiIso_of_comp_right φ φ'
  · intro
    exact quasiIso_comp φ φ'

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