measure_eq_iInf

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

← MathLib Explorer

English

μ s equals the infimum over all measurable supersets t of s of μ t.

Русский

μ s равно инфимуимума от μ t по всем измеримым надмножествам t над s.

LaTeX

$$$\mu s = \bigwedge_{t \; (s \subseteq t)\, (MeasurableSet t)} \mu t$$$

Lean4

theorem measure_eq_iInf (s : Set α) : μ s = ⨅ (t) (_ : s ⊆ t) (_ : MeasurableSet t), μ t := by
  rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]

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

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

Разделы

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

Аффилиация

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