card_Iic_prod

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.card_Iic_prod

English

The cardinality of Iic(x) in the product equals the product of the cardinalities of Iic(x1) and Iic(x2).

Русский

Кардиналильность Iic(x) в произведении равна произведению кардиналитетов Iic(x1) и Iic(x2).

LaTeX

$$$ #(Iic\,x) = #(Iic\,x.1) \cdot #(Iic\,x.2) $$$

Lean4

theorem card_Iic_prod (x : α × β) : #(Iic x) = #(Iic x.1) * #(Iic x.2) :=
  card_product ..

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

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

Разделы

Аффилиация

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