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

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

instance ClopenUpperSet.instPartialOrder {α : Type u_1} [TopologicalSpace α] [LE α] : PartialOrder (ClopenUpperSet α)

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

See Note [custom simps projection].

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.

@[simp]

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

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

theorem ClopenUpperSet.ext_iff {α : Type u_1} [TopologicalSpace α] [LE α] {s t : ClopenUpperSet α} : 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.instMax {α : Type u_1} [TopologicalSpace α] [LE α] : Max (ClopenUpperSet α)

instance ClopenUpperSet.instMin {α : Type u_1} [TopologicalSpace α] [LE α] : Min (ClopenUpperSet α)

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

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

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

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

@[simp]

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

@[simp]

theorem ClopenUpperSet.coe_inf {α : Type u_1} [TopologicalSpace α] [LE α] (s 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 α)