Commit 2021-05-05 18:50 79edde24

View on Github →

feat(topology/discrete_quotient): Add a few lemmas about discrete quotients (#7454) This PR adds the discrete_quotient.map construction and generally improves on the discrete_quotient API.

Estimated changes

Modified src/topology/discrete_quotient.lean

modified def discrete_quotient.comap

added theorem discrete_quotient.comap_comp

added theorem discrete_quotient.comap_id

added theorem discrete_quotient.comap_mono

added def discrete_quotient.le_comap

added theorem discrete_quotient.le_comap_comp

added theorem discrete_quotient.le_comap_id

added theorem discrete_quotient.le_comap_trans

added def discrete_quotient.map

added theorem discrete_quotient.map_comp

added theorem discrete_quotient.map_continuous

added theorem discrete_quotient.map_id

added theorem discrete_quotient.map_of_le

added theorem discrete_quotient.map_of_le_apply

added theorem discrete_quotient.map_proj

added theorem discrete_quotient.map_proj_apply

added theorem discrete_quotient.of_le_comp

added theorem discrete_quotient.of_le_comp_apply

added theorem discrete_quotient.of_le_map

added theorem discrete_quotient.of_le_map_apply

added theorem discrete_quotient.of_le_refl

added theorem discrete_quotient.of_le_refl_apply