instIsCofilteredOrEmptyProd — Mathlib

English

If C and D are IsCofilteredOrEmpty, then their product is IsCofilteredOrEmpty.

Русский

Если C и D кофильтрованы или пусты, то их произведение C × D кофильтровано или пусто.

LaTeX

$$$\\mathrm{IsCofilteredOrEmpty}(C) \\land \\mathrm{IsCofilteredOrEmpty}(D) \\Rightarrow \\mathrm{IsCofilteredOrEmpty}(C \\times D)$$$

Lean4

instance [IsCofilteredOrEmpty C] [IsCofilteredOrEmpty D] : IsCofilteredOrEmpty (C × D)
    where
  cone_objs k
    l :=
    ⟨(min k.1 l.1, min k.2 l.2), (minToLeft k.1 l.1, minToLeft k.2 l.2), (minToRight k.1 l.1, minToRight k.2 l.2),
      trivial⟩
  cone_maps k l f g := ⟨(eq f.1 g.1, eq f.2 g.2), (eqHom f.1 g.1, eqHom f.2 g.2), by simp [eq_condition]⟩

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