card_Icc

Mathlib.Data.Pi.Interval

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

English

For a,b : ∀ i, α(i), the size of the combined interval Ico(a,b) equals the product of the coordinatewise interval sizes minus 1: #(Ico a b) = ∏ i #(Icc(a(i), b(i))) − 1.

Русский

Для функций a,b: ∀ i, α(i) выполняется: |Ico(a,b)| = (∏ᵢ |Icc(a(i), b(i))|) − 1.

LaTeX

$$$$ \\#(Ico(a,b)) = \\prod_{i} \\#(Icc(a(i), b(i))) - 1 $$$$

Lean4

theorem card_Icc : #(Icc a b) = ∏ i, #(Icc (a i) (b i)) :=
  card_piFinset _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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