English
Let i ∈ ι and a, b ∈ α_i. The image of Ioo(a, b) under Pi.mulSingle i is the interval Ioo between Pi.mulSingle i a and Pi.mulSingle i b.
Русский
Пусть i ∈ ι и a, b ∈ α_i. Образ Ioo(a, b) под Pi.mulSingle i есть Ioo( Pi.mulSingle i a, Pi.mulSingle i b ).
LaTeX
$$$ \\mathrm{image}(\\Pi.mulSingle\, i)( \\mathrm{Ioo}(a,b) ) = \\mathrm{Ioo}( \\Pi.mulSingle i\, a, \\Pi.mulSingle i\, b ) $$$
Lean4
@[to_additive]
theorem image_mulSingle_Ioo (i : ι) (a b : α i) :
Pi.mulSingle i '' Ioo a b = Ioo (Pi.mulSingle i a) (Pi.mulSingle i b) :=
image_update_Ioo _ _ _ _