Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-13 17:43 31800d81

View on Github →

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.

Estimated changes

deleted theorem continuous_quotient_lift