coproducts_eq_self — Mathlib

English

If W is stable under coproducts, then coproducts W equals W; i.e., coproducts is the identity on W.

Русский

Если W стабилен относительно копродуктов, то coproducts W равен W; копродукты действуют как тождественный операции на W.

LaTeX

$$coproducts(W) = W \text{(under stability)}$$

Lean4

@[simp]
theorem coproducts_eq_self [IsStableUnderCoproducts.{w} W] : coproducts.{w} W = W :=
  le_antisymm W.coproducts_le W.le_coproducts

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