le_join_apply

Mathlib.MeasureTheory.Measure.GiryMonad

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

← MathLib Explorer

English

For any measurable s, ∫ μ s d m ≤ (join m) s.

Русский

Для любого измеримого s верно неравенство ∫ μ s d m ≤ (join m) s.

LaTeX

$$$\\int⁻ μ, μ(s) \\, d m ≤ (join\\, m)(s).$$$

Lean4

theorem le_join_apply (m : Measure (Measure α)) (s : Set α) : ∫⁻ μ, μ s ∂m ≤ join m s :=
  by
  rw [measure_eq_iInf]
  exact le_iInf₂ fun t hst ↦ le_iInf fun htm ↦ join_apply htm ▸ by gcongr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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