isSifted_iff_asSmallIsSifted — Mathlib

English

A category is sifted iff its AsSmall version is sifted.

Русский

Категория ситообразна тогда и только тогда, когда ее версия AsSmall ситообразна.

LaTeX

$$IsSifted C ↔ IsSifted (AsSmall.C)$$

Lean4

/-- In particular a category is sifted iff and only if it is so when viewed as a small category -/
theorem isSifted_iff_asSmallIsSifted : IsSifted C ↔ IsSifted (AsSmall.{w} C)
    where
  mp _ := isSifted_of_equiv AsSmall.equiv.symm
  mpr _ := isSifted_of_equiv AsSmall.equiv

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