square_commutes — Mathlib

English

The range of the sum_equiv equals the entire GoodProducts set.

Русский

Образ равносильности суммы равен всему GoodProducts.

LaTeX

$$$\\mathrm{range}(\\mathrm{sum\\_equiv}) = \\mathrm{GoodProducts}(C)$$$

Lean4

theorem square_commutes : SumEval C ho ∘ Sum.inl = ModuleCat.ofHom (πs C o) ∘ eval (π C (ord I · < o)) :=
  by
  ext l
  dsimp [SumEval]
  rw [← Products.eval_πs C (Products.prop_of_isGood _ _ l.prop)]
  simp [eval]

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