Theorems · Inductive type · measure theory

MeasureTheory.Measure.Regular

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

A measure μ is regular if - it is finite on all compact sets; - it is outer regular: μ(A) = inf {μ(U) | A ⊆ U open} for A measurable; - it is inner regular for open sets, using compact sets: μ(U) = sup {μ(K) | K ⊆ U compact} for U open.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

61 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

MeasurableSpaceTopologicalSpace