toOuterMeasure_uniformOfFintype_apply

English

Let α be a finite set. The outer measure on α induced by the uniform distribution on α assigns to any subset s ⊆ α the proportion of α that lies in s, i.e. |s| / |α|.

Русский

Пусть α — конечное множество. Внешняя мера, порождаемая равномерным распределением на α, задаёт для любой подзадачи s ⊆ α долю элементов α, входящих в s, то есть |s| / |α|.

LaTeX

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

Lean4

theorem toOuterMeasure_uniformOfFintype_apply [Fintype s] :
    (uniformOfFintype α).toOuterMeasure s = Fintype.card s / Fintype.card α := by
  classical rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype, Finset.card_univ]

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