Clopen upper sets

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

Compact open sets

structure ClopenUpperSet (α : Type u_2) [TopologicalSpace α] [LE α] extends TopologicalSpace.Clopens : Type u_2

The type of clopen upper sets of a topological space.

• carrier : Set α
• isClopen' : IsClopen self.carrier
• upper' : IsUpperSet self.carrier

theorem ClopenUpperSet.upper' {α : Type u_2} [TopologicalSpace α] [LE α] (self : ClopenUpperSet α) : IsUpperSet self.carrier

instance ClopenUpperSet.instSetLike {α : Type u_1} [TopologicalSpace α] [LE α] : SetLike (ClopenUpperSet α) α

Equations

• ClopenUpperSet.instSetLike = { coe := fun (s : ClopenUpperSet α) => s.carrier, coe_injective' := ⋯ }

def ClopenUpperSet.Simps.coe {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) : Set α

See Note [custom simps projection].

Equations

• ClopenUpperSet.Simps.coe s = ↑s

theorem ClopenUpperSet.upper {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) : IsUpperSet ↑s

theorem ClopenUpperSet.isClopen {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) : IsClopen ↑s

def ClopenUpperSet.toUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) : UpperSet α

Reinterpret an upper clopen as an upper set.

Equations

• s.toUpperSet = { carrier := ↑s, upper' := ⋯ }

@[simp]

theorem ClopenUpperSet.toUpperSet_coe {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) : ↑s.toUpperSet = ↑s

theorem ClopenUpperSet.ext {α : Type u_1} [TopologicalSpace α] [LE α] {s : ClopenUpperSet α} {t : ClopenUpperSet α} (h : ↑s = ↑t) : s = t

@[simp]

theorem ClopenUpperSet.coe_mk {α : Type u_1} [TopologicalSpace α] [LE α] (s : TopologicalSpace.Clopens α) (h : IsUpperSet s.carrier) : ↑{ toClopens := s, upper' := h } = ↑s

instance ClopenUpperSet.instSup {α : Type u_1} [TopologicalSpace α] [LE α] : Sup (ClopenUpperSet α)

Equations

• ClopenUpperSet.instSup = { sup := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens ⊔ t.toClopens, upper' := ⋯ } }

instance ClopenUpperSet.instInf {α : Type u_1} [TopologicalSpace α] [LE α] : Inf (ClopenUpperSet α)

Equations

• ClopenUpperSet.instInf = { inf := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens ⊓ t.toClopens, upper' := ⋯ } }

instance ClopenUpperSet.instTop {α : Type u_1} [TopologicalSpace α] [LE α] : Top (ClopenUpperSet α)

Equations

• ClopenUpperSet.instTop = { top := { toClopens := ⊤, upper' := ⋯ } }

instance ClopenUpperSet.instBot {α : Type u_1} [TopologicalSpace α] [LE α] : Bot (ClopenUpperSet α)

Equations

• ClopenUpperSet.instBot = { bot := { toClopens := ⊥, upper' := ⋯ } }

instance ClopenUpperSet.instLattice {α : Type u_1} [TopologicalSpace α] [LE α] : Lattice (ClopenUpperSet α)

Equations

• ClopenUpperSet.instLattice = Function.Injective.lattice SetLike.coe ⋯ ⋯ ⋯

instance ClopenUpperSet.instBoundedOrder {α : Type u_1} [TopologicalSpace α] [LE α] : BoundedOrder (ClopenUpperSet α)

Equations

• ClopenUpperSet.instBoundedOrder = BoundedOrder.lift SetLike.coe ⋯ ⋯ ⋯

@[simp]

theorem ClopenUpperSet.coe_sup {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) (t : ClopenUpperSet α) : ↑(s ⊔ t) = ↑s ∪ ↑t

@[simp]

theorem ClopenUpperSet.coe_inf {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) (t : ClopenUpperSet α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem ClopenUpperSet.coe_top {α : Type u_1} [TopologicalSpace α] [LE α] : ↑⊤ = Set.univ

@[simp]

theorem ClopenUpperSet.coe_bot {α : Type u_1} [TopologicalSpace α] [LE α] : ↑⊥ = ∅

instance ClopenUpperSet.instInhabited {α : Type u_1} [TopologicalSpace α] [LE α] : Inhabited (ClopenUpperSet α)

Equations

• ClopenUpperSet.instInhabited = { default := ⊥ }