Commit 2023-04-20 11:35 485b24ed

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 (see also #18448). Holding PR for mathlib4: leanprover-community/mathlib4#2543