mono — Mathlib

English

There exists a set of full ν-a-measure such that for every a in α, for almost every c, the function q ↦ f(a,c) q is monotone (in q).

Русский

Существует множество с полным по мере ν(a) по a, такое что для почти всех c функция q ↦ f(a,c) q монотонна по q.

LaTeX

$$$\forall a,\;\text{ae}_{c\sim ν(a)}(\text{Monotone}(f(a,c)))$.$$

Lean4

theorem mono (hf : IsRatCondKernelCDFAux f κ ν) (a : α) : ∀ᵐ c ∂(ν a), Monotone (f (a, c)) :=
  by
  unfold Monotone
  simp_rw [ae_all_iff]
  exact fun _ _ hqr ↦ hf.mono' a hqr

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