Theorems · Theorem · measure theory

MeasureTheory.Measure.OuterRegular.comap

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α]
  {mβ : MeasurableSpace β} [inst_3 : TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β) [μ.OuterRegular]
  (f : α ≃ₜ β), (MeasureTheory.Measure.comap (⇑f) μ).OuterRegular

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceBorelSpaceTopologicalSpaceBorelSpaceMeasureTheory.Measure.OuterRegular