Clopen upper sets

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

Compact open sets

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

The type of clopen upper sets of a topological space.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

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

Reinterpret an upper clopen as an upper set.

Equations

• ClopenUpperSet.toUpperSet s = { carrier := ↑s, upper' := (_ : IsUpperSet ↑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.instSupClopenUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] : Sup (ClopenUpperSet α)

Equations

• ClopenUpperSet.instSupClopenUpperSet = { sup := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens ⊔ t.toClopens, upper' := (_ : IsUpperSet (↑s ∪ ↑t.toClopens)) } }

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

Equations

• ClopenUpperSet.instInfClopenUpperSet = { inf := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens ⊓ t.toClopens, upper' := (_ : IsUpperSet (↑s ∩ ↑t.toClopens)) } }

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

Equations

• ClopenUpperSet.instTopClopenUpperSet = { top := { toClopens := ⊤, upper' := (_ : IsUpperSet Set.univ) } }

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

Equations

• ClopenUpperSet.instBotClopenUpperSet = { bot := { toClopens := ⊥, upper' := (_ : IsUpperSet ∅) } }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[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.instInhabitedClopenUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] : Inhabited (ClopenUpperSet α)

Equations

• ClopenUpperSet.instInhabitedClopenUpperSet = { default := ⊥ }