sum — Mathlib

English

The sum of discrete categories is discrete.

Русский

Сумма дискретных категорий дискретна.

LaTeX

$$$\\mathrm{IsDiscrete}(C \\oplus C')$$$

Lean4

/-- A product of discrete categories is discrete. -/
instance sum : IsDiscrete (C ⊕ C')
    where
  subsingleton x
    y :=
    {
      allEq f
        g := by
        cases f <;> cases g
        · case inl x y f g => rw [((by assumption : IsDiscrete C).subsingleton x y).allEq f g]
        · case inr x y f g => rw [((by assumption : IsDiscrete C').subsingleton x y).allEq f g] }
  eq_of_hom {x y}
    f := by
    cases f with
    | inl x y f => rw [(by assumption : IsDiscrete C).eq_of_hom f]
    | inr x y f => rw [(by assumption : IsDiscrete C').eq_of_hom f]

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