restrict_le_self

Mathlib.MeasureTheory.Measure.Restrict

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

← MathLib Explorer

English

If t is a measurable set, then μ|s(t) = μ(t ∩ s).

Русский

Если t измеримо, то μ|s(t) = μ(t ∩ s).

LaTeX

$$$\text{restrict}_{s}(t) = μ(t \cap s)$ for measurable t.$$

Lean4

theorem restrict_le_self : μ.restrict s ≤ μ :=
  Measure.le_iff.2 fun t ht =>
    calc
      μ.restrict s t = μ (t ∩ s) := restrict_apply ht
      _ ≤ μ t := measure_mono inter_subset_left

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

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

Разделы

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

Аффилиация

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