measure_apply

Mathlib.MeasureTheory.Measure.Content

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Content.measure_apply

English

For a measurable set s, μ.measure s equals μ.outerMeasure s.

Русский

Для измеримого множества s выполнено μ.measure s = μ.outerMeasure s.

LaTeX

$$$$\\mu.measure\\,s = μ.outerMeasure\\,s \\quad(\\text{for } s \\text{ measurable}).$$$$

Lean4

theorem measure_apply {s : Set G} (hs : MeasurableSet s) : μ.measure s = μ.outerMeasure s :=
  toMeasure_apply _ _ hs

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

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

Разделы

Аффилиация

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