pi_univ_Ico_subset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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