count_apply_finite' — Mathlib

English

Let s be a finite measurable subset of a measure space. Then the counting measure of s equals the cardinality of s, viewed as an extended nonnegative real.

Русский

Пусть s — конечное измеримое подмножество пространства меры. Тогда счётная мера s равна кардиналу множества s, приведённому к бесконечно-неотрицательному вещественному числу.

LaTeX

$$$count\;s = (s.Finite.toFinset.card).cast$$$

Lean4

theorem count_apply_finite' {s : Set α} (s_fin : s.Finite) (s_mble : MeasurableSet s) : count s = #s_fin.toFinset := by
  simp [← @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]

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