feat(order/directed): Scott continuous functions (#18517)
We prove an insert result for directed sets when the relation is reflexive. This is then used to show that a Scott continuous function is monotone.
This result is required in the [construction of the Scott topology on a preorder](https://github.com/leanprover-community/mathlib4/pull/2508) (see also #18448).
Holding PR for mathlib4: leanprover-community/mathlib4#2543
Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
