Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-30 16:05 7f450cb8

View on Github →

feat(topology/sets/order): Clopen upper sets (#12670) Define clopen_upper_set, the type of clopen upper sets of an ordered topological space.

Estimated changes

Created src/topology/sets/order.lean

added theorem clopen_upper_set.clopen

added theorem clopen_upper_set.coe_bot

added theorem clopen_upper_set.coe_inf

added theorem clopen_upper_set.coe_mk

added theorem clopen_upper_set.coe_sup

added theorem clopen_upper_set.coe_top

added def clopen_upper_set.to_upper_set

added theorem clopen_upper_set.upper

added structure clopen_upper_set