Icc_eq

Mathlib.Data.Pi.Interval

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

English

For a,b : ∀ i, α(i), the interval Icc in the product space equals the product of the coordinatewise intervals: Icc(a,b) = ∏ i Icc(a(i), b(i)).

Русский

Для функций a,b: ι → α(i) выполнено Icc(a,b) = ∏ᵢ Icc(a(i), b(i)).

LaTeX

$$$$ Icc(a,b) = \\prod_{i} Icc\\bigl(a(i), b(i)\\bigr) $$$$

Lean4

theorem Icc_eq : Icc a b = piFinset fun i => Icc (a i) (b i) :=
  rfl

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

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

Разделы

Аффилиация

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