Ici_prod_Ici

Mathlib.Order.Interval.Set.Basic

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

English

Upper-sets multiply to give the upper-set of the pair: Ici a ×ˢ Ici b = Ici (a,b).

Русский

Объединение верхних множеств даёт верхнее множество пары: [a]×[b] = [a,b].

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