Ici_prod_Ici

Mathlib.Order.UpperLower.Prod

URI: https://scilib.ai/kg/mathlib#UpperSet.Ici_prod_Ici

English

The product of principal upper sets at coordinates equals the principal upper set at the product.

Русский

Произведение порожденных верхних множеств по координатам даёт порожденное верхнее множество в произведении.

LaTeX

$$Ici a ×ˢ Ici b = Ici (a, b)$$

Lean4

@[simp]
theorem Ici_prod_Ici (a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b) :=
  rfl

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

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

Разделы

Аффилиация

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