densityProcess_le_one — Mathlib

English

The densityProcess is bounded above by 1: densityProcess ≤ 1 for all arguments.

Русский

DensityProcess не превосходит единицы: densityProcess ≤ 1 для всех аргументов.

LaTeX

$$$\text{densityProcess}(\kappa,\nu,n,a,x,s) \le 1$$$

Lean4

theorem densityProcess_le_one (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (x : γ) (s : Set β) : densityProcess κ ν n a x s ≤ 1 :=
  by
  refine ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.div_le_of_le_mul ?_)
  rw [ENNReal.ofReal_one, one_mul]
  exact meas_countablePartitionSet_le_of_fst_le hκν n a x s

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