isFiniteMeasureRestrict

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

English

If s,t are measurable and μ s ≤ μ t + ε, then μ tᶜ ≤ μ sᶜ + ε for any ε.

Русский

Если s,t измеримы и μ(s) ≤ μ(t) + ε, то μ(t^c) ≤ μ(s^c) + ε для любого ε.

LaTeX

$$MeasurableSet s, MeasurableSet t ⇒ ∀ ε ≥ 0, μ s ≤ μ t + ε ⇒ μ t^c ≤ μ s^c + ε$$

Lean4

instance isFiniteMeasureRestrict (μ : Measure α) (s : Set α) [h : IsFiniteMeasure μ] : IsFiniteMeasure (μ.restrict s) :=
  ⟨by simp⟩

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

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

Разделы

Аффилиация

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