ae_ae_of_ae_join

Mathlib.MeasureTheory.Measure.GiryMonad

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.ae_ae_of_ae_join

English

From an a.e. statement on m.join, conclude a.e. statements on m via ae_join.

Русский

Из утверждения, верного почти всюду для m.join, следует почти всюду для m через ae_join.

LaTeX

$$ae_ae_of_ae_join: (ae m.join) ⇒ (ae m) via ae_join$$

Lean4

theorem ae_ae_of_ae_join {m : Measure (Measure α)} {p : α → Prop} (h : ∀ᵐ a ∂m.join, p a) : ∀ᵐ μ ∂m, ∀ᵐ a ∂μ, p a :=
  le_ae_join m h

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

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

Разделы

Аффилиация

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