Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-20 11:52 52e29379

View on Github →

feat(topology): the currying homeomorphism (#6319)

Estimated changes

Modified src/topology/compact_open.lean

added theorem continuous_map.continuous_curry'

added theorem continuous_map.continuous_curry

added theorem continuous_map.continuous_of_continuous_uncurry

added theorem continuous_map.continuous_uncurry

added theorem continuous_map.continuous_uncurry_of_continuous

added def continuous_map.curry'

added def continuous_map.curry

added def continuous_map.uncurry

added def homeomorph.curry

Modified src/topology/subset_properties.lean