iInf_rat_gt_eq — Mathlib

English

The infimum over rational numbers greater than x of f equals f(x) for Stieltjes f.

Русский

Инфинум над рациональными r>x равен f(x) для Стильтьес-функции.

LaTeX

$$$$\\inf_{r\\in\\mathbb{Q}, x< r} f(r) = f(x).$$$$

Lean4

theorem iInf_rat_gt_eq (f : StieltjesFunction) (x : ℝ) : ⨅ r : { r' : ℚ // x < r' }, f r = f x :=
  by
  rw [← iInf_Ioi_eq f x]
  refine (Real.iInf_Ioi_eq_iInf_rat_gt _ ?_ f.mono).symm
  refine ⟨f x, fun y => ?_⟩
  rintro ⟨y, hy_mem, rfl⟩
  exact f.mono (le_of_lt hy_mem)

Похожие утверждения