Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-14 11:14 2871bd1e

View on Github →

chore(logic/function): drop function.uncurry' (#2678) See [lean#161](https://github.com/leanprover-community/lean/pull/161/files#diff-42c23da308a4d5900f9f3244953701daR132) Also add uniform_continuous.prod_map and uniform_continuous₂.bicompl

Estimated changes

Modified src/logic/function/basic.lean

deleted theorem function.curry_uncurry'

deleted def function.uncurry'

deleted theorem function.uncurry'_bicompr

deleted theorem function.uncurry'_curry

added theorem function.uncurry_bicompl

Modified src/order/filter/extr.lean

Modified src/topology/algebra/group_completion.lean

Modified src/topology/algebra/uniform_ring.lean

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/lipschitz.lean

Modified src/topology/uniform_space/abstract_completion.lean

modified theorem abstract_completion.extension₂_coe_coe

modified theorem abstract_completion.uniform_continuous_map₂

Modified src/topology/uniform_space/basic.lean

added theorem uniform_continuous.prod_map

added theorem uniform_continuous₂.bicompl

added theorem uniform_continuous₂.uniform_continuous

modified def uniform_continuous₂

modified theorem uniform_continuous₂_curry

modified theorem uniform_continuous₂_def

Modified src/topology/uniform_space/completion.lean

modified theorem uniform_space.completion.extension₂_coe_coe

modified theorem uniform_space.completion.map₂_coe_coe

modified theorem uniform_space.completion.uniform_continuous_map₂