Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-23 13:05 34826f0d

View on Github →

feat(order/directed): A few more lemmas (#16953) Simple lemmas about directed.

Estimated changes

added theorem antitone.directed_ge
added theorem antitone.directed_le
added theorem directed_on.mono'
modified theorem directed_on.mono
added theorem monotone.directed_ge