bind_apply_le

Mathlib.MeasureTheory.Measure.GiryMonad

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

← MathLib Explorer

English

For f, with s measurable, bind m f s ≤ ∫ f a s ∂m.

Русский

Для измеримого s верно bound ≤ интеграл

LaTeX

$$$\\text{bind } m\\ f\\ s \\le \\int⁻ a, f a\\, s \\, \\partial m$$$

Lean4

theorem bind_apply_le {m : Measure α} (f : α → Measure β) {s : Set β} (hs : MeasurableSet s) :
    bind m f s ≤ ∫⁻ a, f a s ∂m := by
  rw [bind, join_apply hs]
  apply lintegral_map_le

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

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

Разделы

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

Аффилиация

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