densityProcess_mono_set — Mathlib

English

If ν ≤ ν', then densityProcess(κ, ν') ≤ densityProcess(κ, ν).

Русский

Если ν ≤ ν', то densityProcess(κ, ν') ≤ densityProcess(κ, ν).

LaTeX

$$$\text{densityProcess}(\kappa,ν',n,a,x,s) ≤ \text{densityProcess}(\kappa,ν,n,a,x,s)$$$

Lean4

theorem densityProcess_mono_set (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (x : γ) {s s' : Set β} (h : s ⊆ s') :
    densityProcess κ ν n a x s ≤ densityProcess κ ν n a x s' :=
  by
  unfold densityProcess
  obtain h₀ | h₀ := eq_or_ne (ν a (countablePartitionSet n x)) 0
  · simp [h₀]
  · gcongr
    simp only [ne_eq, ENNReal.div_eq_top, h₀, and_false, false_or, not_and, not_not]
    exact eq_top_mono (meas_countablePartitionSet_le_of_fst_le hκν n a x s')

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