Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-07 19:53 940d3713

View on Github →

feat(topology/instances/add_circle): generalize homeo_Icc_quot from ℝ to archimedean groups (#17983)

Add left/right/two-sided continuity results about to_Ico/Ioc_mod and equiv_Ico.
Add tfae_to_Ico_eq_to_Ioc which states 8 other equivalent conditions for to_Ico_mod and to_Ioc_mod to agree at a point, from this comment in #17933.

Estimated changes

Modified src/algebra/order/to_interval_mod.lean

added theorem Ico_eq_locus_Ioc_eq_Union_Ioo

added def mem_Ioo_mod

added theorem mem_Ioo_mod_iff_eq_mod_zmultiples

added theorem mem_Ioo_mod_iff_sub_ne_zsmul

added theorem mem_Ioo_mod_iff_to_Ico_div_add_one_ne_to_Ioc_div

added theorem mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div

added theorem mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod

added theorem mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod

added theorem mem_Ioo_mod_iff_to_Ico_mod_ne_left

added theorem mem_Ioo_mod_iff_to_Ioc_mod_ne_right

added theorem tfae_mem_Ioo_mod

Modified src/topology/instances/add_circle.lean

modified theorem add_circle.coe_add_period

added theorem add_circle.coe_image_Ioc_eq

added theorem add_circle.continuous_at_equiv_Ico

added theorem add_circle.continuous_at_equiv_Ioc

added theorem add_circle.continuous_equiv_Ioc_symm

deleted theorem add_circle.eq_of_end_ident

added theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ico_mod

added theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ioc_mod

added def add_circle.equiv_Ioc

modified def add_circle.homeo_Icc_quot

modified theorem add_circle.lift_Ico_continuous

modified theorem add_circle.lift_Ico_eq_lift_Icc

modified theorem add_circle.lift_Ico_zero_coe_apply

modified theorem add_circle.lift_Ico_zero_continuous

added def add_circle.lift_Ioc

added theorem add_circle.lift_Ioc_coe_apply

added theorem continuous_at_to_Ico_mod

added theorem continuous_at_to_Ioc_mod

added theorem continuous_left_to_Ioc_mod

added theorem continuous_right_to_Ico_mod

added theorem to_Ico_mod_eventually_eq_to_Ioc_mod