quasiIso_ιTruncLE_iff_isSupported

English

For any K and e, IsIso (K.ιTruncLE e) is equivalent to K.IsStrictlySupported e.

Русский

Для любых K и e изоморфизм IsIso (K.ιTruncLE e) эквивалентен K.IsStrictlySupported e.

LaTeX

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

Lean4

theorem quasiIso_ιTruncLE_iff_isSupported : QuasiIso (K.ιTruncLE e) ↔ K.IsSupported e :=
  by
  rw [← quasiIso_opFunctor_map_iff, ← isSupported_op_iff]
  exact K.op.quasiIso_πTruncGE_iff_isSupported e.op

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