pi_univ_Iic

Mathlib.Order.Interval.Set.Pi

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

English

For a family of preorders (αi), the product of the intervals Iic(xi) over all i equals Iic(x).

Русский

Для семейства порядков (α_i) произведение интервалов Iic(x_i) по всем i равно Iic(x).

LaTeX

$$$$ (\pi\mathrm{univ} \; (\lambda i.\Iic(x_i))) = \Iic(x) $$$$

Lean4

@[simp]
theorem pi_univ_Iic : (pi univ fun i ↦ Iic (x i)) = Iic x :=
  ext fun y ↦ by simp [Pi.le_def]

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

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

Разделы

Аффилиация

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