uIcc_eq

Mathlib.Data.Pi.Interval

URI: https://scilib.ai/kg/mathlib#Pi.uIcc_eq

English

For functions a,b : ι → α i, the uIcc on the product equals the coordinatewise product of uIcc intervals: uIcc(a,b) = piFinset_i (uIcc(a(i), b(i))).

Русский

Для функций a,b: ι → α(i) выполняется uIcc(a,b) = piFinset_i (uIcc(a(i), b(i))).

LaTeX

$$$$ uIcc(a,b) = \\pi\\mathrm{Finset}_{i \\in ι}\\, uIcc(a_i, b_i) $$$$

Lean4

theorem uIcc_eq : uIcc a b = piFinset fun i => uIcc (a i) (b i) :=
  rfl

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

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

Разделы

Аффилиация

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