image_mulSingle_uIcc — Mathlib

English

The image of uIcc(a, b) under Pi.mulSingle i is the uIcc between Pi.mulSingle i a and Pi.mulSingle i b.

Русский

Образ uIcc(a, b) под Pi.mulSingle i равен uIcc( Pi.mulSingle i a, Pi.mulSingle i b ).

LaTeX

$$$ \\mathrm{image}(\\Pi.mulSingle\, i)( \\mathrm{uIcc}(a,b) ) = \\mathrm{uIcc}( \\Pi.mulSingle i\, a, \\Pi.mulSingle i\, b ) $$$

Lean4

@[to_additive]
theorem image_mulSingle_uIcc (i : ι) (a b : α i) :
    Pi.mulSingle i '' uIcc a b = uIcc (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_uIcc _ _ _ _

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