apply_union_le

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.apply_union_le

← MathLib Explorer

English

Subadditivity of probability measures: μ(s1 ∪ s2) ≤ μ(s1) + μ(s2).

Русский

Субаддитивность распределения: μ(s1 ∪ s2) ≤ μ(s1) + μ(s2).

LaTeX

$$μ(s_1 \\cup s_2) \\le μ(s_1) + μ(s_2)$$

Lean4

theorem apply_union_le (μ : ProbabilityMeasure Ω) {s₁ s₂ : Set Ω} : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ :=
  by
  rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]
  exact FiniteMeasure.apply_union_le _

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

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

Разделы

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

Аффилиация

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