image_mulSingle_Ioo_right — Mathlib

English

Let i ∈ ι and b ∈ α_i. The image of Ioo(1, b) under Pi.mulSingle i equals Ioo(1, Pi.mulSingle i b).

Русский

Пусть i ∈ ι и b ∈ α_i. Образ Ioo(1, b) под Pi.mulSingle i равен Ioo(1, Pi.mulSingle i b).

LaTeX

$$$ \\mathrm{image}(\\Pi.mulSingle\, i)( \\mathrm{Ioo}(1,b) ) = \\mathrm{Ioo}(1, \\Pi.mulSingle i\, b) $$$

Lean4

@[to_additive]
theorem image_mulSingle_Ioo_right (i : ι) (b : α i) : Pi.mulSingle i '' Ioo 1 b = Ioo 1 (Pi.mulSingle i b) :=
  image_update_Ioo_right _ _ _

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