bddBelow_range — Mathlib

English

For hf, a.e. c, and every q ∈ ℚ, the range of r ↦ f(a,c) r over r>I q is bounded below (by 0).

Русский

Для а.е. c и каждого q ∈ ℚ множество значений f(a,c) r по r>q ограничено снизу (не меньше 0).

LaTeX

$$$\forall a,\text{ae}_{c\sim ν(a)}(\forall q\in\mathbb{Q},\; \operatorname{BddBelow}(\operatorname{range}(r\mapsto f(a,c)r)\, \text{on } Ioi(q))).$$$

Lean4

theorem bddBelow_range (hf : IsRatCondKernelCDFAux f κ ν) (a : α) :
    ∀ᵐ t ∂(ν a), ∀ q : ℚ, BddBelow (range fun (r : Ioi q) ↦ f (a, t) r) :=
  by
  filter_upwards [hf.nonneg a] with c hc
  refine fun q ↦ ⟨0, ?_⟩
  simp [mem_lowerBounds, hc]

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