le_measure_diff

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.le_measure_diff

← MathLib Explorer

English

We have μ(s1) − μ(s2) ≤ μ(s1 \\ s2).

Русский

Существует неравенство μ(s1) − μ(s2) ≤ μ(s1 \\ s2).

LaTeX

$$$$ \\mu(s_{1}) - \\mu(s_{2}) \\le \\mu\\left(s_{1} \\setminus s_{2}\\right). $$$$

Lean4

theorem le_measure_diff : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂) :=
  tsub_le_iff_left.2 <| (measure_le_inter_add_diff μ s₁ s₂).trans <| by gcongr; apply inter_subset_right

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

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

Разделы

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

Аффилиация

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