card_Ici_prod

Mathlib.Order.Interval.Finset.Defs

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

English

The cardinality of the product of two lower intervals equals the product of their cardinalities.

Русский

Кардиналность произведения нижних интервалов равна произведению их кардиналитетов.

LaTeX

$$$ \#(\mathrm{Ici}\ x) = \#(\mathrm{Ici}\ x.1) \cdot \#(\mathrm{Ici}\ x.2) $$$

Lean4

theorem card_Ici_prod (x : α × β) : #(Ici x) = #(Ici x.1) * #(Ici x.2) :=
  card_product _ _

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

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

Разделы

Аффилиация

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