image_mulSingle_Ico_right — Mathlib

English

Let i ∈ ι and b ∈ α_i. The image of Ico(f(i), b) under Pi.mulSingle i is the interval Ico f (update f i b).

Русский

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

LaTeX

$$$ \\mathrm{image}(\\Pi.mulSingle\, i)( \\mathrm{Ico}(f(i), b) ) = \\mathrm{Ico}( f, \\mathrm{update}(f,i)(b) ) $$$

Lean4

@[to_additive]
theorem image_mulSingle_Ico_right (i : ι) (b : α i) : Pi.mulSingle i '' Ico 1 b = Ico 1 (Pi.mulSingle i b) :=
  image_update_Ico_right _ _ _

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