card_Iio

Mathlib.Data.DFinsupp.Interval

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

English

The cardinality of Iio f equals the product of Iic cards over the support of f, minus one.

Русский

Кардинал Iio f равен произведению кардиналов Iic(f(i)) по i из поддержки f, минус 1.

LaTeX

$$card_Iio : #(Iio f) = (\prod i ∈ f.support, #(Iic (f i))) - 1$$

Lean4

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

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

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

Разделы

Аффилиация

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