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