English
Let R be a complete linear order and f: ι → R. If sup_i f(i) ∉ range(f), then the union over i of the left-closed intervals Iic(f(i)) equals the left-open interval Iio(sup_i f(i)).
Русский
Пусть R — полная линейная упорядоченность и есть функция f: ι → R. Если верхняя грань по f не достигается элементом из образа range(f), то объединение интервалов слева ℐic(f(i)) равно интервалу слева от sup_i f(i).
LaTeX
$$$$\left( \sup_{i} f(i) \notin \operatorname{range}(f) \right) \Rightarrow \bigcup_{i} \mathrm{Iic}(f(i)) = \mathrm{Iio}\left(\sup_{i} f(i)\right).$$$$
Lean4
theorem iUnion_Iic_eq_Iio_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R}
(no_greatest_elem : (⨆ i, f i) ∉ range f) : ⋃ i : ι, Iic (f i) = Iio (⨆ i, f i) :=
@iUnion_Ici_eq_Ioi_iInf ι (OrderDual R) _ f no_greatest_elem
