Commit 2023-02-13 09:48 5bed97b4

View on Github →

feat: port Topology.Sets.Order (#2232)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/UpperLower/Basic.lean

added def LowerSet.Simps.coe

added def UpperSet.Simps.coe

Created Mathlib/Topology/Sets/Order.lean

added def ClopenUpperSet.Simps.coe

added theorem ClopenUpperSet.clopen

added theorem ClopenUpperSet.coe_bot

added theorem ClopenUpperSet.coe_inf

added theorem ClopenUpperSet.coe_mk

added theorem ClopenUpperSet.coe_sup

added theorem ClopenUpperSet.coe_top

added def ClopenUpperSet.toUpperSet

added theorem ClopenUpperSet.upper

added structure ClopenUpperSet