le_count_apply — Mathlib

English

A technical inequality about sums and counts showing that cumulative measures bound counts.

Русский

Техническое неравенство о суммах и счетах, показывающее ограничение счетчика суммарной меры.

LaTeX

$$$$\\text{(Inequality relating sums and counts)}$$$$

Lean4

theorem le_count_apply : ∑' _ : s, (1 : ℝ≥0∞) ≤ count s :=
  calc
    (∑' _ : s, 1 : ℝ≥0∞) = ∑' i, indicator s 1 i := tsum_subtype s 1
    _ ≤ ∑' i, dirac i s := (ENNReal.tsum_le_tsum fun _ => le_dirac_apply)
    _ ≤ count s := le_sum_apply _ _

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