mulSingle_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mulSingle_inf [∀ i, SemilatticeInf (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_inf _ _ _ _

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