pi_univ_Ici — Mathlib

English

For a family of preorders (αi) indexed by i, the product of the intervals Ici(xi) over all i is equal to Ici(x) where x is the family (xi)i.

Русский

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

LaTeX

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

Lean4

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

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