apply_mono

Mathlib.MeasureTheory.Measure.FiniteMeasure

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

← MathLib Explorer

English

Reiterates that monotonicity μ(s1) ≤ μ(s2) holds when s1 ⊆ s2.

Русский

Повторно утверждается неубывающее свойство β(с) при вложении.

LaTeX

$$μ (s1) ≤ μ (s2) for s1 ⊆ s2$$

Lean4

theorem apply_mono (μ : FiniteMeasure Ω) {s₁ s₂ : Set Ω} (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ :=
  ENNReal.toNNReal_mono (measure_ne_top _ s₂) ((μ : Measure Ω).mono h)

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

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

Разделы

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

Аффилиация

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