pi_univ_Ioo_subset — Mathlib

English

For a family of preorders (αi), the pi-universal image of Iio(xi) is contained in Iio(x).

Русский

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

LaTeX

$$$$ (\pi univ\; (\lambda i. Iio(x_i))) \subseteq Iio(x) $$$$

Lean4

theorem pi_univ_Ioo_subset [Nonempty ι] : (pi univ fun i ↦ Ioo (x i) (y i)) ⊆ Ioo x y := fun _ hx ↦
  ⟨(pi_univ_Ioi_subset _) fun i hi ↦ (hx i hi).1, (pi_univ_Iio_subset _) fun i hi ↦ (hx i hi).2⟩

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