toFinite_apply_eq_zero_iff

Mathlib.MeasureTheory.Measure.WithDensityFinite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.toFinite_apply_eq_zero_iff

English

For [SFinite μ], μ.toFinite(s) = 0 iff μ(s) = 0 for any set s.

Русский

Для [SFinite μ] для любого множества s справедливо μ.toFinite(s) = 0 тогда и только тогда, когда μ(s) = 0.

LaTeX

$$$ μ^{toFinite}(s) = 0 \iff μ(s) = 0 $$$

Lean4

@[simp]
theorem toFinite_apply_eq_zero_iff [SFinite μ] {s : Set α} : μ.toFinite s = 0 ↔ μ s = 0 := by
  simp only [← compl_mem_ae_iff, ae_toFinite]

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

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

Разделы

Аффилиация

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