isFiltered_of_representablyCoflat

Mathlib.CategoryTheory.Filtered.Flat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isFiltered_of_representablyCoflat

← MathLib Explorer

English

Same as 66656: the equivalence between hf.functor.Final and the directed-le condition.

Русский

То же самое, что и выше: эквивалентность между hf.functor.Final и условием направленности по порядку.

LaTeX

$$Same as 66656$$

Lean4

theorem isFiltered_of_representablyCoflat [IsFiltered D] [RepresentablyCoflat F] : IsFiltered C :=
  isFiltered_of_isFiltered_costructuredArrow F (𝟭 _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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