quasiIso_truncLEMap_iff — Mathlib

English

QuasiIso (truncLEMap φ e) iff for all i,i' with e.f i = i', QuasiIsoAt φ i'.

Русский

QuasiIso (truncLEMap φ e) эквивалентно тому, что для всех i,i' с e.f i = i' выполняется QuasiIsoAt φ i'.

LaTeX

$$$ QuasiIso\big( truncLEMap\ \varphi\ e \big) \iff \forall i:\iota\, \forall i':\iota',\ e.f i=i' \to\ QuasiIsoAt\big(\varphi\big) i' $$$

Lean4

theorem quasiIso_truncLEMap_iff : QuasiIso (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i' :=
  by
  rw [← quasiIso_opFunctor_map_iff]
  simp only [← quasiIsoAt_opFunctor_map_iff φ]
  apply quasiIso_truncGEMap_iff

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