measure_compl

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

If s is measurable and μ s ≠ ∞, then μ sᶜ = μ univ − μ s.

Русский

Если s измеримо и μ(s) ≠ ∞, то μ sᶜ = μ(полное множество) − μ(s).

LaTeX

$$$$ \\mu(s^{\\mathrm{c}}) = \\mu(\\mathsf{univ}) - \\mu(s). $$$$

Lean4

theorem measure_compl (h₁ : MeasurableSet s) (h_fin : μ s ≠ ∞) : μ sᶜ = μ univ - μ s :=
  measure_compl₀ h₁.nullMeasurableSet h_fin

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

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

Разделы

Аффилиация

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