Theorems · Inductive type · measure theory

MeasureTheory.Measure.WeaklyRegular

{α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → Prop

A measure μ is weakly regular if - it is outer regular: μ(A) = inf {μ(U) | A ⊆ U open} for A measurable; - it is inner regular for open sets, using closed sets: μ(U) = sup {μ(F) | F ⊆ U closed} for U open.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

31 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

MeasurableSpaceTopologicalSpace