Commit 2023-04-17 12:04 9a88da83

View on Github →

chore: fix names in DiscreteQuotient (#3481)

Estimated changes

Modified Mathlib/Topology/DiscreteQuotient.lean

added theorem DiscreteQuotient.LEComap.comp

added theorem DiscreteQuotient.LEComap.mono

added def DiscreteQuotient.LEComap

deleted theorem DiscreteQuotient.LeComap.comp

deleted theorem DiscreteQuotient.LeComap.mono

deleted def DiscreteQuotient.LeComap

added theorem DiscreteQuotient.fiber_subset_ofLE

deleted theorem DiscreteQuotient.fiber_subset_ofLe

modified theorem DiscreteQuotient.leComap_id

modified theorem DiscreteQuotient.leComap_id_iff

modified def DiscreteQuotient.map

modified theorem DiscreteQuotient.map_comp

added theorem DiscreteQuotient.map_comp_ofLE

deleted theorem DiscreteQuotient.map_comp_ofLe

modified theorem DiscreteQuotient.map_comp_proj

modified theorem DiscreteQuotient.map_continuous

added theorem DiscreteQuotient.map_ofLE

deleted theorem DiscreteQuotient.map_ofLe

modified theorem DiscreteQuotient.map_proj

added def DiscreteQuotient.ofLE

added theorem DiscreteQuotient.ofLE_comp_map

added theorem DiscreteQuotient.ofLE_comp_ofLE

added theorem DiscreteQuotient.ofLE_comp_proj

added theorem DiscreteQuotient.ofLE_continuous

added theorem DiscreteQuotient.ofLE_map

added theorem DiscreteQuotient.ofLE_ofLE

added theorem DiscreteQuotient.ofLE_proj

added theorem DiscreteQuotient.ofLE_refl

added theorem DiscreteQuotient.ofLE_refl_apply

deleted def DiscreteQuotient.ofLe

deleted theorem DiscreteQuotient.ofLe_comp_map

deleted theorem DiscreteQuotient.ofLe_comp_ofLe

deleted theorem DiscreteQuotient.ofLe_comp_proj

deleted theorem DiscreteQuotient.ofLe_continuous

deleted theorem DiscreteQuotient.ofLe_map

deleted theorem DiscreteQuotient.ofLe_ofLe

deleted theorem DiscreteQuotient.ofLe_proj

deleted theorem DiscreteQuotient.ofLe_refl

deleted theorem DiscreteQuotient.ofLe_refl_apply