count_singleton' — Mathlib

English

The counting measure of a singleton set {a} equals 1, provided the singleton {a} is measurable.

Русский

Счётная мера множества {a} равна 1 при условии измеримости множества {a}.

LaTeX

$$$count\;\{a\} = 1$$$

Lean4

@[simp]
theorem count_singleton' {a : α} (ha : MeasurableSet ({ a } : Set α)) : count ({ a } : Set α) = 1 :=
  by
  rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]
  simp []

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