count_apply_finset'

Mathlib.MeasureTheory.Measure.Count

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

English

For a finite set s (as a Finset), count (↑s) equals card of s.

Русский

Для конечного множества s (Finset) count(↑s) равно card(s).

LaTeX

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

Lean4

@[simp]
theorem count_apply_finset' {s : Finset α} (hs : MeasurableSet (s : Set α)) : count (↑s : Set α) = #s := by
  simp [count_apply hs]

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

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

Разделы

Аффилиация

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