English
If f is monotone, g is antitone, and f ≤ g, then the supremum of f lies inside every interval [f(n), g(n)].
Русский
Если f монотонна, g антомонтонна и выполняется неравенство f ≤ g, то верхняя грань последовательности f(n) принадлежит каждому интервалу [f(n), g(n)].
LaTeX
$$$f: \beta \to α$ is monotone, $g: \beta \to α$ is antitone, and $h: f \le g$. Then $\bigvee_{n} f(n) \in \bigcap_{n} [f(n), g(n)].$$$
Lean4
/-- **Nested intervals lemma**: if `f` is a monotone sequence, `g` is an antitone sequence, and
`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
theorem ciSup_mem_iInter_Icc_of_antitone [SemilatticeSup β] {f g : β → α} (hf : Monotone f) (hg : Antitone g)
(h : f ≤ g) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
by
refine mem_iInter.2 fun n => ?_
haveI : Nonempty β := ⟨n⟩
have : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
exact ⟨le_ciSup ⟨g <| n, forall_mem_range.2 this⟩ _, ciSup_le this⟩
