quasiIsoAt_ιTruncLE — Mathlib

English

IsIso (K.ιTruncLE e) iff K is strictly supported with respect to e.

Русский

IsIso (K.ιTruncLE e) эквивалентно тому, что K строго поддержано относительно e.

LaTeX

$$$ IsIso (K.ιTruncLE e) \iff K.IsStrictlySupported e $$$

Lean4

theorem quasiIsoAt_ιTruncLE {j : ι} {j' : ι'} (hj' : e.f j = j') : QuasiIsoAt (K.ιTruncLE e) j' :=
  by
  have := K.op.quasiIsoAt_πTruncGE e.op hj'
  exact inferInstanceAs (QuasiIsoAt ((unopFunctor _ _).map (K.op.πTruncGE e.op).op) j')

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