Ici_prod_def

Mathlib.Order.Interval.Finset.Defs

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

English

In the product order, the upper interval Ici(x) is the product of the upper intervals of its coordinates.

Русский

В порядке произведения верхний интервал Ici(x) равен произведению верхних интервалов координат.

LaTeX

$$$ Ici x = Ici x.1 \timesˢ Ici x.2 $$$

Lean4

theorem Ici_prod_def (x : α × β) : Ici x = Ici x.1 ×ˢ Ici x.2 :=
  rfl

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

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

Разделы

Аффилиация

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