Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-18 11:38 04206afe

View on Github →

feat(topology/instances): add_circle = interval with ends identified (#17889)

Estimated changes

Modified src/topology/instances/add_circle.lean

added theorem add_circle.coe_add_period

added theorem add_circle.coe_eq_coe_iff_of_mem_Ico

modified theorem add_circle.coe_image_Icc_eq

modified theorem add_circle.coe_image_Ico_eq

modified theorem add_circle.continuous_equiv_Ico_symm

added inductive add_circle.endpoint_ident

added theorem add_circle.eq_of_end_ident

added def add_circle.equiv_Icc_quot

modified def add_circle.equiv_Ico

added def add_circle.homeo_Icc_quot

added def add_circle.lift_Ico

added theorem add_circle.lift_Ico_coe_apply

added theorem add_circle.lift_Ico_continuous

added theorem add_circle.lift_Ico_eq_lift_Icc

added theorem add_circle.lift_Ico_zero_coe_apply

added theorem add_circle.lift_Ico_zero_continuous