Commit 2019-11-18 02:08 7c5f282d

View on Github →

chore(algebra/order_functions): rename min/max_distrib_of_monotone (#1697) New names monotone.map_min/max better align with monoid_hom.map_mul etc.

Estimated changes

Modified src/algebra/order_functions.lean

deleted theorem max_distrib_of_monotone

deleted theorem min_distrib_of_monotone

added theorem monotone.map_max

added theorem monotone.map_min

Modified src/topology/metric_space/basic.lean