iInf_rat_gt_eq — Mathlib

English

For almost every b, and every rational q, the infimum over rationals r > q of f(a,b)(r) equals f(a,b)(q).

Русский

Для почти всех b и каждого рационального q наименьшее значение f(a,b)(r) при r > q равно f(a,b)(q).

LaTeX

$$$\\forall a, \\text{ae}_{b\\sim ν(a)}\\;\\forall q\\in\\mathbb{Q}, \\; \\inf_{r>q} f(a,b)(r) = f(a,b)(q).$$$

Lean4

theorem iInf_rat_gt_eq (hf : IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ b ∂(ν a), ∀ q, ⨅ r : Ioi q, f (a, b) r = f (a, b) q := by
  filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.iInf_rat_gt_eq

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