Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-18 13:38 ff3130da

View on Github →

feat(topology/constructions): topology on ulift (#2716)

Estimated changes

Modified src/topology/constructions.lean

added theorem continuous_ulift_down

added theorem continuous_ulift_up

Modified src/topology/homeomorph.lean

added def homeomorph.{u