Lean4
/-- The natural map from `[a, a + p] ⊂ 𝕜` with endpoints identified to `𝕜 / ℤ • p`, as a
homeomorphism of topological spaces. -/
def homeoIccQuot [TopologicalSpace 𝕜] [OrderTopology 𝕜] : 𝕋 ≃ₜ Quot (EndpointIdent p a)
where
toEquiv := equivIccQuot p a
continuous_toFun :=
by
simp_rw [isQuotientMap_quotient_mk'.continuous_iff, continuous_iff_continuousAt,
continuousAt_iff_continuous_left_right]
intro x; constructor
on_goal 1 => erw [equivIccQuot_comp_mk_eq_toIocMod]
on_goal 2 => erw [equivIccQuot_comp_mk_eq_toIcoMod]
all_goals
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
rw [IsInducing.subtypeVal.continuousWithinAt_iff]
· apply continuous_left_toIocMod
· apply continuous_right_toIcoMod
continuous_invFun := continuous_quot_lift _ ((AddCircle.continuous_mk' p).comp continuous_subtype_val)
