isCocontinuous_comp — Mathlib

English

If G is J–K cocontinuous and G' is K–L cocontinuous, then their composition G ⋙ G' is J–L cocontinuous.

Русский

Если G коконтинуальна по J–K и G' по K–L, то их композиция коконтинуальна по J–L.

LaTeX

$$$[G.IsCocontinuous\\ J\\ K] \\land [G'.IsCocontinuous\\ K\\ L] \\Rightarrow (G \\cdot G').IsCocontinuous\\ J\\ L$$$

Lean4

/-- The composition of two cocontinuous functors is cocontinuous. -/
theorem isCocontinuous_comp [G.IsCocontinuous J K] [G'.IsCocontinuous K L] : (G ⋙ G').IsCocontinuous J L where
  cover_lift h := G.cover_lift J K (G'.cover_lift K L h)

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