mulSingle_sup — Mathlib

English

If each f i has a SemilatticeSup and a One, then Pi.mulSingle i (x ⊔ y) = Pi.mulSingle i x ⊔ Pi.mulSingle i y.

Русский

Пусть каждый f i имеет SemilatticeSup и единицу. Тогда Pi.mulSingle i (x ⊔ y) = Pi.mulSingle i x ⊔ Pi.mulSingle i y.

LaTeX

$$$ \mathrm{Pi.mulSingle} \ i (x \sqcup y) = \mathrm{Pi.mulSingle} \ i x \sqcup \mathrm{Pi.mulSingle} \ i y $$$

Lean4

@[to_additive]
theorem mulSingle_sup [∀ i, SemilatticeSup (f i)] [∀ i, One (f i)] (i : I) (x y : f i) :
    Pi.mulSingle i (x ⊔ y) = Pi.mulSingle i x ⊔ Pi.mulSingle i y :=
  Function.update_sup _ _ _ _

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