iUnion_Iio — Mathlib

English

Assume α has no maximum element. Then every x ∈ α belongs to some open interval of the form Iio(a) = {y | y < a}, hence ⋃_{a∈α} Iio(a) = univ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iUnion_Iio [NoMaxOrder α] : ⋃ a : α, Iio a = univ :=
  iUnion_eq_univ_iff.2 exists_gt

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