frequently_ae_iff

Mathlib.MeasureTheory.OuterMeasure.AE

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

English

A property p holds frequently almost everywhere with respect to μ iff μ({a : p(a)}) ≠ 0.

Русский

Свойство p встречается часто almost everywhere по μ тогда, когда μ({a : p(a)}) ≠ 0.

LaTeX

$$$\mathrm{Frequently}\,(p, \mathrm{ae}\,\mu) \iff \mu(\{a : p(a)\}) \neq 0$$$

Lean4

theorem frequently_ae_iff {p : α → Prop} : (∃ᵐ a ∂μ, p a) ↔ μ {a | p a} ≠ 0 :=
  not_congr compl_mem_ae_iff

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

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

Разделы

Аффилиация

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