Theorems · Definition · measure theory

AddCircle.measurableEquivIco

(T : ℝ) → [hT : Fact (0 < T)] → (a : ℝ) → AddCircle T ≃ᵐ ↑(Set.Ico a (a + T))

The isomorphism AddCircle T ≃ Ico a (a + T) whose inverse is the natural quotient map, as an equivalence of measurable spaces.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Fact