measure_zero

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

URI: https://scilib.ai/kg/mathlib#Set.Finite.measure_zero

English

If s is finite, then μ(s) = 0 when μ has no atoms.

Русский

Если s конечно и μ без атомов, то μ(s) = 0.

LaTeX

$$$$s \text{ finite } \Rightarrow μ(s) = 0.$$$$

Lean4

theorem _root_.Set.Finite.measure_zero (h : s.Finite) (μ : Measure α) [NoAtoms μ] : μ s = 0 :=
  h.countable.measure_zero μ

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

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

Разделы

Аффилиация

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