image_mulSingle_Icc — Mathlib

English

Let i ∈ ι and a, b ∈ α_i. The image of Icc(a, b) under the map Pi.mulSingle i is the interval Icc between Pi.mulSingle i a and Pi.mulSingle i b.

Русский

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

LaTeX

$$$ \\text{image}(\\Pi.mulSingle\, i)\ \bigl( \\mathrm{Icc}(a,b) \\bigr) = \\mathrm{Icc}( \\Pi.mulSingle i\, a, \\Pi.mulSingle i\, b ) $$$

Lean4

@[to_additive]
theorem image_mulSingle_Icc (i : ι) (a b : α i) :
    Pi.mulSingle i '' Icc a b = Icc (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_Icc _ _ _ _

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