English
Let f: R → R be monotone and bounded below on the interval (x, ∞). Then the infimum of f over (x, ∞) equals the infimum of f over rational points strictly greater than x; i.e. the greatest lower bound of the tail is the same whether one samples along all reals r > x or along rational r > x.
Русский
Пусть f: ℝ → ℝ монотонна и снизу ограничена на интервале (x, ∞). Тогда инфимум функции на (x, ∞) равен инфимуму функции на рациональных точках, больших x; т. е. наибольшая нижняя граница хвоста совпадает при выборе всех действительных r > x и при выборе только рациональных r > x.
LaTeX
$$$\\forall f:\\mathbb{R}\\to\\mathbb{R},\\forall x\\in\\mathbb{R},\\left(\\operatorname{BddBelow}(f(Ioi(x))) \\wedge \\operatorname{Monotone}(f)\\right) \\Rightarrow \\inf_{r>x} f(r) = \\inf_{q \\in \\{ q' \\in \\mathbb{Q} \\mid x < q' \\}} f(q).$$
Lean4
theorem iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Ioi x)) (hf_mono : Monotone f) :
⨅ r : Ioi x, f r = ⨅ q : { q' : ℚ // x < q' }, f q :=
by
refine le_antisymm ?_ ?_
· have : Nonempty { r' : ℚ // x < ↑r' } :=
by
obtain ⟨r, hrx⟩ := exists_rat_gt x
exact ⟨⟨r, hrx⟩⟩
refine le_ciInf fun r => ?_
obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop
refine ciInf_set_le hf (hxy.trans ?_)
exact_mod_cast hyr
· refine le_ciInf fun q => ?_
have hq := q.prop
rw [mem_Ioi] at hq
obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq
refine (ciInf_le ?_ ?_).trans ?_
· refine ⟨hf.some, fun z => ?_⟩
rintro ⟨u, rfl⟩
suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
exact ⟨u, u.prop, rfl⟩
· exact ⟨y, hxy⟩
· refine hf_mono (le_trans ?_ hyq.le)
norm_cast
