Icc_eq_pi

Mathlib.Analysis.BoxIntegral.Box.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Box.Icc_eq_pi

English

Box.Icc I equals the product over i of Icc(I.lower i, I.upper i).

Русский

Box.Icc I равно произведению по i из Icc(I.lower i, I.upper i).

LaTeX

$$$ Box.Icc I = \\pi univ \\; (i \\mapsto \\mathrm{Icc}(I.lower i)(I.upper i)) $$$

Lean4

theorem Icc_eq_pi : Box.Icc I = pi univ fun i ↦ Icc (I.lower i) (I.upper i) :=
  (pi_univ_Icc _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru