Theorems · Theorem · measure theory

MeasureTheory.Measure.Regular.restrict_of_measure_ne_top

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α]
  [BorelSpace α] [μ.Regular] {A : Set α}, μ A ≠ ⊤ → (μ.restrict A).Regular

The restriction of a regular measure to a set of finite measure is regular.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

0 results in Mathlib

Foundations

Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceR1SpaceBorelSpaceMeasureTheory.Measure.Regular