Clopen upper sets #

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

Compact open sets #

source

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

Type u_3

carrier : Set α
clopen' : IsClopen s.carrier
upper' : IsUpperSet s.carrier

The type of clopen upper sets of a topological space.

Instances For

source

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

SetLike (ClopenUpperSet α) α

source

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

Set α

See Note [custom simps projection].

Instances For

source

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

IsUpperSet ↑s

source

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

IsClopen ↑s

source

@[simp]

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

↑(ClopenUpperSet.toUpperSet s) = ↑s

source

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

UpperSet α

Reinterpret an upper clopen as an upper set.

Instances For

source

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

s = t

source

@[simp]

theorem ClopenUpperSet.coe_mk {α : Type u_1} [TopologicalSpace α] [LE α] (s : TopologicalSpace.Clopens α) (h : IsUpperSet s.carrier) :

↑{ toClopens := s, upper' := h } = ↑s

source

instance ClopenUpperSet.instSupClopenUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] :

Sup (ClopenUpperSet α)

source

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

Inf (ClopenUpperSet α)

source

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

Top (ClopenUpperSet α)

source

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

Bot (ClopenUpperSet α)

source

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

Lattice (ClopenUpperSet α)

source

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

BoundedOrder (ClopenUpperSet α)

source

@[simp]

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

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

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

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

theorem ClopenUpperSet.coe_top {α : Type u_1} [TopologicalSpace α] [LE α] :

↑⊤ = Set.univ

source

@[simp]

theorem ClopenUpperSet.coe_bot {α : Type u_1} [TopologicalSpace α] [LE α] :

↑⊥ = ∅

source

instance ClopenUpperSet.instInhabitedClopenUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] :

Inhabited (ClopenUpperSet α)