mathlib3
31800d81 - refactor(topology/constructions): review `quotient` API (#15986)

Commit
3 years ago
refactor(topology/constructions): review `quotient` API (#15986) * rename `continuous_quotient_lift` to `continuous.quotient_lift`; * rename `continuous_quotient_lift_on'` to `continuous.quotient_lift_on'`; * add `continuous.quotient_map'` and use it to golf some proofs.
Author
Parents
Loading