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
- carrier : Set α
- clopen' : IsClopen s.carrier
- upper' : IsUpperSet s.carrier
The type of clopen upper sets of a topological space.
Instances For
instance
ClopenUpperSet.instSetLikeClopenUpperSet
{α : Type u_1}
[TopologicalSpace α]
[LE α]
:
SetLike (ClopenUpperSet α) α
def
ClopenUpperSet.Simps.coe
{α : Type u_1}
[TopologicalSpace α]
[LE α]
(s : ClopenUpperSet α)
:
Set α
See Note [custom simps projection].
Instances For
theorem
ClopenUpperSet.upper
{α : Type u_1}
[TopologicalSpace α]
[LE α]
(s : ClopenUpperSet α)
:
IsUpperSet ↑s
theorem
ClopenUpperSet.clopen
{α : 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.
Instances For
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 α)
instance
ClopenUpperSet.instInfClopenUpperSet
{α : Type u_1}
[TopologicalSpace α]
[LE α]
:
Inf (ClopenUpperSet α)
instance
ClopenUpperSet.instTopClopenUpperSet
{α : Type u_1}
[TopologicalSpace α]
[LE α]
:
Top (ClopenUpperSet α)
instance
ClopenUpperSet.instBotClopenUpperSet
{α : Type u_1}
[TopologicalSpace α]
[LE α]
:
Bot (ClopenUpperSet α)
@[simp]
theorem
ClopenUpperSet.coe_sup
{α : Type u_1}
[TopologicalSpace α]
[LE α]
(s : ClopenUpperSet α)
(t : ClopenUpperSet α)
:
@[simp]
theorem
ClopenUpperSet.coe_inf
{α : Type u_1}
[TopologicalSpace α]
[LE α]
(s : ClopenUpperSet α)
(t : ClopenUpperSet α)
:
@[simp]