ae_of_all

Mathlib.MeasureTheory.OuterMeasure.AE

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

English

Reiterates that if p holds for all elements, then p holds almost everywhere.

Русский

Повторение: если p выполняется для всех элементов, тогда p выполняется почти всюду.

LaTeX

$$$(\forall a, p(a)) \Rightarrow \forall^{\text{ae}} a\, p(a)$$$

Lean4

theorem ae_of_all {p : α → Prop} (μ : F) : (∀ a, p a) → ∀ᵐ a ∂μ, p a :=
  Eventually.of_forall

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

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

Разделы

Аффилиация

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