Theorems · Inductive type · measure theory

MeasureTheory.Measure.InnerRegularCompactLTTop

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

A measure μ is inner regular for finite measure sets with respect to compact sets: for any measurable set s with finite measure, then μ(s) = sup {μ(K) | K ⊆ s compact}. The main interest of this class is that it is satisfied for both natural Haar measures (the regular one and the inner regular one).

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

48 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

MeasurableSpaceTopologicalSpace