count_real_singleton' — Mathlib

English

The real-valued counting measure of a singleton equals 1 if the singleton is measurable.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem _root_.MeasureTheory.count_real_singleton' {a : α} (ha : MeasurableSet ({ a } : Set α)) :
    count.real ({ a } : Set α) = 1 := by rw [measureReal_def, count_singleton' ha, ENNReal.toReal_one]

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