English
If [f(n), g(n)] is an antitone sequence of nonempty closed intervals, then the supremum of f(n) lies in all the intervals [f(n), g(n)].
Русский
Если последовательность интервалов [f(n), g(n)] является анти-моннотонной и интервалы непустые, то верхняя граница последовательности f(n) принадлежит всем интервалам [f(n), g(n)].
LaTeX
$$$\bigvee_{n} f(n) \in \bigcap_{n} [f(n), g(n)].$$$
Lean4
/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
theorem ciSup_mem_iInter_Icc_of_antitone_Icc [SemilatticeSup β] {f g : β → α} (h : Antitone fun n => Icc (f n) (g n))
(h' : ∀ n, f n ≤ g n) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
Monotone.ciSup_mem_iInter_Icc_of_antitone (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
(fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'
