English
There is a measurable equivalence between AddCircle T and Ioc a (a+T) with inverse given by the natural quotient map.
Русский
Существует измеримо-изоморфизм между AddCircle(T) и Ioc(a,a+T) с обратной связью, заданной естественным факторным отображением.
LaTeX
$$$\\text{AddCircle}(T) \\cong^m \\mathrm{Ioc}(a,a+T)$ with inverse given by the quotient map$$
Lean4
/-- The isomorphism `AddCircle T ≃ Ioc a (a + T)` whose inverse is the natural quotient map,
as an equivalence of measurable spaces. -/
noncomputable def measurableEquivIoc (a : ℝ) : AddCircle T ≃ᵐ Ioc a (a + T)
where
toEquiv := equivIoc T a
measurable_toFun :=
measurable_of_measurable_on_compl_singleton _
(continuousOn_iff_continuous_restrict.mp <|
continuousOn_of_forall_continuousAt fun _x hx => continuousAt_equivIoc T a hx).measurable
measurable_invFun := AddCircle.measurable_mk'.comp measurable_subtype_coe
