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](leanprover-community/mathlib4#2508) (see also #18448).

Holding PR for mathlib4: leanprover-community/mathlib4#2543



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>

Matches leanprover-community/mathlib3#18517

This result is required in #2508.



Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>

Introduce the Scott topology on a preorder, defined in terms of directed sets.

There is already a related notion of Scott topology defined in `topology.omega_complete_partial_order`, where it is defined on ω-complete partial orders in terms of ω-chains. In some circumstances the definition given here coincides with that given in `topology.omega_complete_partial_order` but in general they are different. Abramsky and Jung ([Domain Theory, 2.2.4][abramsky_gabbay_maibaum_1994]) argue that the ω-chain approach has pedagogical advantages, but the directed sets approach is more appropriate as a theoretical foundation.



Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>

Introduce the Scott topology on a preorder, defined in terms of directed sets.

There is already a related notion of Scott topology defined in `topology.omega_complete_partial_order`, where it is defined on ω-complete partial orders in terms of ω-chains. In some circumstances the definition given here coincides with that given in `topology.omega_complete_partial_order` but in general they are different. Abramsky and Jung ([Domain Theory, 2.2.4][abramsky_gabbay_maibaum_1994]) argue that the ω-chain approach has pedagogical advantages, but the directed sets approach is more appropriate as a theoretical foundation.



Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>

… Mathlib (#11710)

Introduces the Lawson Topology on a preorder.

The Lawson Topology is defined as the meet of the [Lower Topology](leanprover-community/mathlib3#17426) and the [Scott Topology](#2508) previously introduced.

A basis for the Lawson Topology is defined and some basic results are established:

- An upper set is Lawson open if and only if it is Scott open
- A lower set is Lawson closed if and only if it is closed under sups of directed sets
- The Lawson topology on a partial order is T₀ 



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>

… Mathlib (#11710)

Introduces the Lawson Topology on a preorder.

The Lawson Topology is defined as the meet of the [Lower Topology](leanprover-community/mathlib3#17426) and the [Scott Topology](#2508) previously introduced.

A basis for the Lawson Topology is defined and some basic results are established:

- An upper set is Lawson open if and only if it is Scott open
- A lower set is Lawson closed if and only if it is closed under sups of directed sets
- The Lawson topology on a partial order is T₀ 



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>

… Mathlib (#11710)

Introduces the Lawson Topology on a preorder.

The Lawson Topology is defined as the meet of the [Lower Topology](leanprover-community/mathlib3#17426) and the [Scott Topology](#2508) previously introduced.

A basis for the Lawson Topology is defined and some basic results are established:

- An upper set is Lawson open if and only if it is Scott open
- A lower set is Lawson closed if and only if it is closed under sups of directed sets
- The Lawson topology on a partial order is T₀ 



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>

…ogy (#16523)

Unify Scott Topologies, following on from #13201 and #16826.

Originally Mathlib had a notion of ω-Scott Continuity and ω-Scott Topology based on Chains for ω-complete partial orders. Previously we introduced a notion of Scott Continuity and Scott Topology based on directed sets for arbitrary pre-orders (#2508). In #13201, we generalised our definition of Scott Continuity to include ω-Scott Continuity as a special case. This PR continues that work by generalising our notion of Scott Topology to include ω-Scott Topology as a special case.

`Topology.IsScott.scottContinuous_iff_continuous` and `Topology.IsScott.ωscottContinuous_iff_continuous` have almost identical proofs and are presumably special cases of a more general result that I have not yet formulated. However I think this PR covers enough ground to be worth considering at this stage.



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>