count_apply_finset

Mathlib.MeasureTheory.Measure.Count

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.count_apply_finset

English

If α has measurable singleton sets, then count on ↑s equals card of s.

Русский

Если множества содержат единичные множества, тогда count(↑s) = card(s).

LaTeX

$$$$\\mathrm{count}(\\uparrow s) = s.card.$$$$

Lean4

@[simp]
theorem count_apply_finset [MeasurableSingletonClass α] (s : Finset α) : count (↑s : Set α) = #s :=
  count_apply_finset' s.measurableSet

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru