iInf_Ioi_eq — Mathlib

English

The infimum of f over the open interval (x,∞) equals f(x) for a Stieltjes function.

Русский

Значение инфима f на открытом интервале (x,∞) равно f(x) для функции Стильтьеса.

LaTeX

$$$$\\inf_{r> x} f(r) = f(x).$$$$

Lean4

theorem iInf_Ioi_eq (f : StieltjesFunction) (x : ℝ) : ⨅ r : Ioi x, f r = f x :=
  by
  suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]
  rw [f.mono.rightLim_eq_sInf, sInf_image']
  rw [← neBot_iff]
  infer_instance

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