pi_univ_uIcc — Mathlib

English

In the product order, the product over i of the intervals uIcc(a_i, b_i) equals the interval uIcc(a, b) in the product.

Русский

В порядке произведения произведение по i интервалов uIcc(a_i, b_i) равно интервалу uIcc(a, b) в произведении.

LaTeX

$$$ \\bigl(\\pi\\_{\mathrm{univ}}\, (i \\mapsto \\mathrm{uIcc}(a_i,b_i))\\bigr) = \\mathrm{uIcc}(a,b) $$$

Lean4

@[simp]
theorem pi_univ_uIcc (a b : ∀ i, α i) : (pi univ fun i => uIcc (a i) (b i)) = uIcc a b :=
  pi_univ_Icc _ _

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