mathlib3

093aef54 - feat(order/monotone): Functions from/to subsingletons are monotone (#10903)

feat(order/monotone): Functions from/to subsingletons are monotone (#10903) A few really trivial results about monotonicity/antitonicity of `f : α → β` where `subsingleton α` or `subsingleton β`. Also fixes the markdown heading levels in this file