English
Let R be a complete linear order and f: ι → R. If the infimum of f lies in the range of f, then the union over i of Ici(f(i)) equals Ici(inf_i f(i)).
Русский
Пусть R — полная линейная упорядоченность и есть функция f: ι → R. Если наименьшая граница множества {f(i)} достигается в образе, то объединение интервалов слева Ici(f(i)) равно Ici(inf_i f(i)).
LaTeX
$$$$\left( \inf_{i} f(i) \in \operatorname{range}(f) \right) \Rightarrow \bigcup_{i} \mathrm{Ici}(f(i)) = \mathrm{Ici}\left(\inf_{i} f(i)\right).$$$$
Lean4
theorem iUnion_Ici_eq_Ici_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R} (has_least_elem : (⨅ i, f i) ∈ range f) :
⋃ i : ι, Ici (f i) = Ici (⨅ i, f i) := by
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range, iUnion_exists,
iUnion_iUnion_eq']
