toMeasure_uniformOfFinset_apply — Mathlib

English

For the finite uniform distribution on s, toMeasure equals the discrete uniform density on s.

Русский

Для дискретного равномерного распределения на s мера toMeasure совпадает с дискретной плотностью на s.

LaTeX

$$$\\text{toMeasureUniformOfFinset}(s,hs)\\;\\toMeasure = \\text{finiteUniformDensity on } s$$$

Lean4

@[simp]
theorem toMeasure_uniformOfFinset_apply [MeasurableSpace α] (ht : MeasurableSet t) :
    (uniformOfFinset s hs).toMeasure t = #({x ∈ s | x ∈ t}) / #s :=
  (toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_uniformOfFinset_apply hs t)

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