Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monotone_comp

Modification history

2019-09-28 22:44

src/order/basic.lean

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

Deleted monotone_comp View on Github →

2017-07-23 18:29

algebra/order.lean

refactor(*): use 'lemma' iff statement is private

Modified monotone_comp View on Github →

2017-07-23 15:16

algebra/order.lean

refactor(*): import content from lean/library/data and library_dev

Added monotone_comp View on Github →