antitone functions (#13079)

Commit

3 years ago

feat(order/bounds): Boundedness of monotone/antitone functions (#13079) Co-authored-by: Mantas Bakšys <39908973+MantasBaksys@users.noreply.github.com>

Author

MantasBaksys

Parents

0dde2cb8

mathlib3 57f382a0 - feat(order/bounds): Boundedness of monotone/antitone functions (#13079)

mathlib3
57f382a0 - feat(order/bounds): Boundedness of monotone/antitone functions (#13079)