Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-28 22:44 30aa8d2f

View on Github →

chore(order/basic): rename monotone_comp to monotone.comp, reorder arguments (#1497)

Estimated changes

Modified src/order/basic.lean

deleted theorem monotone_comp

Modified src/order/filter/lift.lean

Modified src/order/fixed_points.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/cauchy.lean

Modified src/topology/uniform_space/completion.lean