quasiIso_truncLEMap_iff — Mathlib

English

QuasiIso (truncLEMap φ n) iff ∀ i, i ≤ n ⇒ QuasiIsoAt φ i.

Русский

QuasiIso(truncLEMap φ n) эквивалентно ∀ i ≤ n, QuasiIsoAt φ i.

LaTeX

$$$ \\text{QuasiIso}(\\mathrm{truncLEMap}\\, \\varphi\\, n) \\Leftrightarrow \\forall i,\\ i \\le n \\Rightarrow \\text{QuasiIsoAt}(\\varphi, i) $$$

Lean4

theorem quasiIso_truncLEMap_iff : QuasiIso (truncLEMap φ n) ↔ ∀ (i : ℤ) (_ : i ≤ n), QuasiIsoAt φ i :=
  by
  rw [HomologicalComplex.quasiIso_truncLEMap_iff]
  constructor
  · intro h i hi
    obtain ⟨k, rfl⟩ := Int.le.dest hi
    exact h k _ (by dsimp; cutsat)
  · rintro h i i' rfl
    exact h _ (by dsimp; cutsat)

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