Iic_prod_Iic

Mathlib.Order.Interval.Set.Basic

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

English

Lower-sets multiply to give a lower-set of a pair: Iic a × Iic b = Iic (a,b).

Русский

Множество пар (x,y) с x ≤ a и y ≤ b есть эквивалентно нижнему множеству пары (a,b).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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