instIsFilteredOrEmptyProd — Mathlib

English

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

Русский

Если C и D имеют свойство IsFilteredOrEmpty, то их произведение C × D также IsFilteredOrEmpty.

LaTeX

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

Lean4

instance [IsFilteredOrEmpty C] [IsFilteredOrEmpty D] : IsFilteredOrEmpty (C × D)
    where
  cocone_objs k
    l :=
    ⟨(max k.1 l.1, max k.2 l.2), (leftToMax k.1 l.1, leftToMax k.2 l.2), (rightToMax k.1 l.1, rightToMax k.2 l.2),
      trivial⟩
  cocone_maps k l f g := ⟨(coeq f.1 g.1, coeq f.2 g.2), (coeqHom f.1 g.1, coeqHom f.2 g.2), by simp [coeq_condition]⟩

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