coeq_condition

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCardinalFiltered.coeq_condition

← MathLib Explorer

English

From IsCardinalFiltered J κ, conclude IsFiltered J.

Русский

Из IsCardinalFiltered J κ следует IsFiltered J.

LaTeX

$$$IsFiltered(J)$$$

Lean4

@[reassoc]
theorem coeq_condition (k : K) : f k ≫ coeqHom f hK = toCoeq f hK :=
  (cocone (parallelFamily f) (hasCardinalLT_arrow_walkingParallelFamily hK hκ.out.aleph0_le)).w (.line k)

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

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

Разделы

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

Аффилиация

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