Theorems · Theorem · measure theory

AddCircle.add_projection_respects_measure

∀ (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) {U : Set (AddCircle T)},
  MeasurableSet U → MeasureTheory.volume U = MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' U ∩ Set.Ioc t (t + T))

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Cited by

2 results in Mathlib

Foundations

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

Assumes

Fact