comp — Mathlib

English

If F and G are RepresentablyCoflat, then F ⋙ G is RepresentablyCoflat.

Русский

Если F и G RepresentablyCoflat, то F ⋙ G RepresentablyCoflat.

LaTeX

$$$$ \\mathrm{RepresentablyCoflat}(F) \\land \\mathrm{RepresentablyCoflat}(G) \\Rightarrow \\mathrm{RepresentablyCoflat}(F \\!\\cdot G). $$$$

Lean4

instance comp (G : D ⥤ E) [RepresentablyCoflat F] [RepresentablyCoflat G] : RepresentablyCoflat (F ⋙ G) :=
  (representablyFlat_op_iff _).1 <| inferInstanceAs <| RepresentablyFlat (F.op ⋙ G.op)

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