quasiIso_opMap — Mathlib

English

Similar to the previous result, but in the opposite direction: if φ is quasi-iso, then opMap φ is quasi-iso.

Русский

Аналогично предыдущему, но в обратном направлении: если φ — квазиизоморфизм, то opMap φ — квазиизоморфизм.

LaTeX

$$$\operatorname{QuasiIso}(φ) \Rightarrow \operatorname{QuasiIso}(\operatorname{opMap}(φ))$$$

Lean4

theorem quasiIso_opMap (φ : S₁ ⟶ S₂) [QuasiIso φ] : QuasiIso (opMap φ) :=
  by
  rw [quasiIso_opMap_iff]
  infer_instance

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