isFiltered — Mathlib

English

An Ind-object A implies that the CostructuredArrow yoneda A is filtered.

Русский

Ind-объект A подразумевает, что CostructuredArrow yoneda A является фильтрованным.

LaTeX

$$$\mathrm{IsIndObject}(A)\Rightarrow \mathrm{IsFiltered}(\mathrm{CostructuredArrow}(\mathrm{yoneda},A))$$$

Lean4

theorem isFiltered (h : IsIndObject A) : IsFiltered (CostructuredArrow yoneda A) :=
  IsFiltered.of_final h.presentation.toCostructuredArrow

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