# Clopen upper sets #

In this file we define the type of clopen upper sets.

### Compact open sets #

structure ClopenUpperSet (α : Type u_3) [] [LE α] extends :
Type u_3

The type of clopen upper sets of a topological space.

Instances For
theorem ClopenUpperSet.upper' {α : Type u_3} [] [LE α] (self : ) :
IsUpperSet self.carrier
instance ClopenUpperSet.instSetLike {α : Type u_1} [] [LE α] :
Equations
• ClopenUpperSet.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }
def ClopenUpperSet.Simps.coe {α : Type u_1} [] [LE α] (s : ) :
Set α

See Note [custom simps projection].

Equations
Instances For
theorem ClopenUpperSet.upper {α : Type u_1} [] [LE α] (s : ) :
theorem ClopenUpperSet.isClopen {α : Type u_1} [] [LE α] (s : ) :
@[simp]
theorem ClopenUpperSet.toUpperSet_coe {α : Type u_1} [] [LE α] (s : ) :
s.toUpperSet = s
def ClopenUpperSet.toUpperSet {α : Type u_1} [] [LE α] (s : ) :

Reinterpret an upper clopen as an upper set.

Equations
• s.toUpperSet = { carrier := s, upper' := }
Instances For
theorem ClopenUpperSet.ext {α : Type u_1} [] [LE α] {s : } {t : } (h : s = t) :
s = t
@[simp]
theorem ClopenUpperSet.coe_mk {α : Type u_1} [] [LE α] (s : ) (h : IsUpperSet s.carrier) :
{ toClopens := s, upper' := h } = s
instance ClopenUpperSet.instSup {α : Type u_1} [] [LE α] :
Equations
• ClopenUpperSet.instSup = { sup := fun (s t : ) => { toClopens := s.toClopens t.toClopens, upper' := } }
instance ClopenUpperSet.instInf {α : Type u_1} [] [LE α] :
Equations
• ClopenUpperSet.instInf = { inf := fun (s t : ) => { toClopens := s.toClopens t.toClopens, upper' := } }
instance ClopenUpperSet.instTop {α : Type u_1} [] [LE α] :
Equations
• ClopenUpperSet.instTop = { top := { toClopens := , upper' := } }
instance ClopenUpperSet.instBot {α : Type u_1} [] [LE α] :
Equations
• ClopenUpperSet.instBot = { bot := { toClopens := , upper' := } }
instance ClopenUpperSet.instLattice {α : Type u_1} [] [LE α] :
Equations
instance ClopenUpperSet.instBoundedOrder {α : Type u_1} [] [LE α] :
Equations
@[simp]
theorem ClopenUpperSet.coe_sup {α : Type u_1} [] [LE α] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem ClopenUpperSet.coe_inf {α : Type u_1} [] [LE α] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem ClopenUpperSet.coe_top {α : Type u_1} [] [LE α] :
= Set.univ
@[simp]
theorem ClopenUpperSet.coe_bot {α : Type u_1} [] [LE α] :
=
instance ClopenUpperSet.instInhabited {α : Type u_1} [] [LE α] :
Equations
• ClopenUpperSet.instInhabited = { default := }