toMeasure_uniformOfFintype_apply — Mathlib

English

Let α be a finite set and s a measurable subset. The measure on α induced by the uniform distribution satisfies μ(s) = |s| / |α|.

Русский

Пусть α — конечное множество и s — измеримое подмножество. Мера на α, порождаемая равномерным распределением, удовлетворяет μ(s) = |s| / |α|.

LaTeX

$$$$ (uniformOfFintype\\, \\alpha).toMeasure(s) = \\frac{|s|}{|\\alpha|} $$$$

Lean4

theorem toMeasure_uniformOfFintype_apply [MeasurableSpace α] (hs : MeasurableSet s) [Fintype s] :
    (uniformOfFintype α).toMeasure s = Fintype.card s / Fintype.card α := by
  classical simp [uniformOfFintype, Fintype.card_subtype, hs]

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