density_nonneg — Mathlib

English

For all a, x, and s, density κ ν a x s ≥ 0.

Русский

Для любых a, x и s, density κ ν a x s ≥ 0.

LaTeX

$$0 ≤ density κ ν a x s$$

Lean4

theorem density_nonneg (hκν : fst κ ≤ ν) (a : α) (x : γ) (s : Set β) : 0 ≤ density κ ν a x s :=
  by
  refine le_limsup_of_frequently_le ?_ ?_
  · exact Frequently.of_forall (fun n ↦ densityProcess_nonneg _ _ _ _ _ _)
  · exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

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