isIso_post — Mathlib

English

If IsFiltered CostructuredArrow yoneda A holds, then limit.post K A is iso.

Русский

Пусть IsFiltered CostructuredArrow yoneda A выполняется, тогда limit.post K A изоморфизм.

LaTeX

$$$\operatorname{IsFiltered}(\operatorname{CostructuredArrow}(\mathrm{yoneda}, A)) \Rightarrow \operatorname{IsIso}(\operatorname{limit.post}(K, A))$$$

Lean4

theorem isIso_post [IsFiltered (CostructuredArrow yoneda A)] : IsIso (limit.post K A) :=
  iso_hom A K ▸ inferInstance

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