final_of_isFiltered_structuredArrow

English

Alternative presentation: If given the same hypotheses as 66607, then A is filtered.

Русский

Альтернативное изложение: при тех же предположениях, что и в 66607, A фильтрована.

LaTeX

$$$\\bigl( \\text{IsFiltered}(B) \\land \\text{Final}(R) \\land \\forall b, \\mathrm{IsFiltered}(\\mathrm{CostructuredArrow}\\, L (R.obj\\, b)) \\bigr) \\Rightarrow \\mathrm{IsFiltered}(A)$$$

Lean4

/-- If `StructuredArrow d F` is filtered for any `d : D`, then `F : C ⥤ D` is final. This is
simply because filtered categories are connected. More profoundly, the converse is also true if
`C` is filtered, see `final_iff_isFiltered_structuredArrow`. -/
theorem final_of_isFiltered_structuredArrow [∀ d, IsFiltered (StructuredArrow d F)] : Final F where
  out _ := IsFiltered.isConnected _

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