image_mulSingle_Icc_left — Mathlib

English

Let i ∈ ι and a ∈ α_i. The image of Icc(a, 1) under Pi.mulSingle i is the interval Icc(a, 1) moved to the i-th coordinate.

Русский

Пусть i ∈ ι и a ∈ α_i. Образ Icc(a,1) под Pi.mulSingle i равен Icc(a,1) в отношении i-й координаты.

LaTeX

$$$ \\mathrm{image}(\\Pi.mulSingle\, i)( \\mathrm{Icc}(a,1) ) = \\mathrm{Icc}( \\Pi.mulSingle i\, a, 1 ) $$$

Lean4

@[to_additive]
theorem image_mulSingle_Icc_left (i : ι) (a : α i) : Pi.mulSingle i '' Icc a 1 = Icc (Pi.mulSingle i a) 1 :=
  image_update_Icc_left _ _ _

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