mathlib
36c09f7b - doc(order/*): use "monotone" / "antitone" in place of "monotonically increasing" / "monotonically decreasing" (#9408)

Commit
4 years ago
doc(order/*): use "monotone" / "antitone" in place of "monotonically increasing" / "monotonically decreasing" (#9408) This PR cleans up the references to monotone and antitone function in lemmas and docstrings. It doesn't touch anything beyond the docstrings. Co-authored-by: Oliver Nash <github@olivernash.org>
Author
Parents
Loading