apply_mono

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

← MathLib Explorer

English

Monotonicity of a probability measure: if s1 ⊆ s2 then μ s1 ≤ μ s2.

Русский

Монотонность распределения: если s1 ⊆ s2, то μ(s1) ≤ μ(s2).

LaTeX

$$s_1 \\subseteq s_2 \\Rightarrow μ(s_1) \\le μ(s_2)$$

Lean4

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

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

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

Разделы

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

Аффилиация

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