isSiftedOrEmpty

Mathlib.CategoryTheory.Filtered.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsFilteredOrEmpty.isSiftedOrEmpty

English

If C is filtered-or-empty, then C is sifted-or-empty.

Русский

Если C фильтрована-или-пустая, тогда C является sifted-или-пустой.

LaTeX

$$IsSiftedOrEmpty C$$

Lean4

theorem isSiftedOrEmpty [IsFilteredOrEmpty C] : IsSiftedOrEmpty C :=
  Functor.final_diag_of_isFiltered

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru