English
Let R be a complete linear order and f: ι → R. If the supremum of f lies in the range of f, then the union over i of Iic(f(i)) equals Iic(sup_i f(i)).
Русский
Пусть R — полная линейная упорядоченность и есть функция f: ι → R. Если supremum множества значений f достигается некоторым f(i), то объединение интервалов слева Iic(f(i)) равно Iic( sup_i f(i) ).
LaTeX
$$$$\left( \sup_{i} f(i) \in \operatorname{range}(f) \right) \Rightarrow \bigcup_{i} \mathrm{Iic}(f(i)) = \mathrm{Iic}\left(\sup_{i} f(i)\right).$$$$
Lean4
theorem iUnion_Iic_eq_Iic_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R}
(has_greatest_elem : (⨆ i, f i) ∈ range f) : ⋃ i : ι, Iic (f i) = Iic (⨆ i, f i) :=
@iUnion_Ici_eq_Ici_iInf ι (OrderDual R) _ f has_greatest_elem
