Commit 2023-09-08 07:26 8cad453e

View on Github →

feat: Functoriality of WithUpperSetTopology (#6988) A monotone map between preorders spaces induces a continuous map between themselves considered with the upper set topology. Similarly for the lower set topology.

Estimated changes

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

added theorem WithLowerSetTopology.IsLowerSet_toLowerSet_preimage

added theorem WithLowerSetTopology.isOpen_ofLowerSet_preimage

added def WithLowerSetTopology.map

added theorem WithLowerSetTopology.map_comp

added theorem WithLowerSetTopology.map_id

added theorem WithLowerSetTopology.ofLowerSet_le_ofLowerSet

added theorem WithLowerSetTopology.toLowerSet_specializes_toLowerSet

modified def WithLowerSetTopology

added theorem WithUpperSetTopology.IsUpperSet_toUpperSet_preimage

added theorem WithUpperSetTopology.isOpen_ofUpperSet_preimage

added def WithUpperSetTopology.map

added theorem WithUpperSetTopology.map_comp

added theorem WithUpperSetTopology.map_id

added theorem WithUpperSetTopology.ofUpperSet_le_ofUpperSet

added theorem WithUpperSetTopology.toUpperSet_specializes_toUpperSet

modified def WithUpperSetTopology