iUnion_Ioi — Mathlib

English

Assume α has no minimum element. Then every x ∈ α belongs to some interval Ioi(a) = {y | y > a}, hence ⋃_{a} Ioi(a) = univ.

Русский

Пусть в α нет минимального элемента. Тогда любой x принадлежит некоторому интервалу Ioi(a) = {y | y > a}, следовательно ⋃_{a} Ioi(a) = всё множество.

LaTeX

$$$$\bigcup_{a\in\alpha} Ioi(a) = \mathrm{univ}$$$$

Lean4

@[simp]
theorem iUnion_Ioi [NoMinOrder α] : ⋃ a : α, Ioi a = univ :=
  iUnion_eq_univ_iff.2 exists_lt

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