# mathlibdocumentation

topology.sets.order

# Clopen upper sets #

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

### Compact open sets #

structure clopen_upper_set (α : Type u_3) [has_le α] :
Type u_3
• to_clopens :
• upper' :

The type of clopen upper sets of a topological space.

Instances for clopen_upper_set
@[protected, instance]
def clopen_upper_set.set_like {α : Type u_1} [has_le α] :
α
Equations
theorem clopen_upper_set.upper {α : Type u_1} [has_le α] (s : clopen_upper_set α) :
theorem clopen_upper_set.clopen {α : Type u_1} [has_le α] (s : clopen_upper_set α) :
@[simp]
theorem clopen_upper_set.to_upper_set_carrier {α : Type u_1} [has_le α] (s : clopen_upper_set α) :
def clopen_upper_set.to_upper_set {α : Type u_1} [has_le α] (s : clopen_upper_set α) :

Reinterpret a upper clopen as an upper set.

Equations
@[protected, ext]
theorem clopen_upper_set.ext {α : Type u_1} [has_le α] {s t : clopen_upper_set α} (h : s = t) :
s = t
@[simp]
theorem clopen_upper_set.coe_mk {α : Type u_1} [has_le α] (h : is_upper_set s.carrier) :
{to_clopens := s, upper' := h} = s
@[protected, instance]
def clopen_upper_set.has_sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def clopen_upper_set.has_inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def clopen_upper_set.has_top {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def clopen_upper_set.has_bot {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def clopen_upper_set.lattice {α : Type u_1} [has_le α] :
Equations
• clopen_upper_set.lattice = clopen_upper_set.lattice._proof_1 clopen_upper_set.lattice._proof_2 clopen_upper_set.lattice._proof_3
@[protected, instance]
def clopen_upper_set.bounded_order {α : Type u_1} [has_le α] :
Equations
@[simp]
theorem clopen_upper_set.coe_sup {α : Type u_1} [has_le α] (s t : clopen_upper_set α) :
(s t) = s t
@[simp]
theorem clopen_upper_set.coe_inf {α : Type u_1} [has_le α] (s t : clopen_upper_set α) :
(s t) = s t
@[simp]
theorem clopen_upper_set.coe_top {α : Type u_1} [has_le α] :
@[simp]
theorem clopen_upper_set.coe_bot {α : Type u_1} [has_le α] :
@[protected, instance]
def clopen_upper_set.inhabited {α : Type u_1} [has_le α] :
Equations