card_Iio

Mathlib.Data.Pi.Interval

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

English

For b : ∀ i, α i, the Iic intervals multiply: #(Iic b) = ∏ i #(Iic (b i)).

Русский

Для b : ∀ i, α i выполняется: #(Iic b) = ∏ i #(Iic(b i)).

LaTeX

$$$$ #(Iic b) = \\prod_{i} #(Iic (b i)) $$$$

Lean4

theorem card_Iio : #(Iio b) = ∏ i, #(Iic (b i)) - 1 := by rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

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

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

Разделы

Аффилиация

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