mathlib documentation

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) [topological_space α] [has_le α] :
Type u_3

The type of clopen upper sets of a topological space.

Instances for clopen_upper_set
@[protected, instance]
Equations
theorem clopen_upper_set.upper {α : Type u_1} [topological_space α] [has_le α] (s : clopen_upper_set α) :
theorem clopen_upper_set.clopen {α : Type u_1} [topological_space α] [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} [topological_space α] [has_le α] {s t : clopen_upper_set α} (h : s = t) :
s = t
@[simp]
theorem clopen_upper_set.coe_mk {α : Type u_1} [topological_space α] [has_le α] (s : topological_space.clopens α) (h : is_upper_set s.carrier) :
{to_clopens := s, upper' := h} = s
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem clopen_upper_set.coe_sup {α : Type u_1} [topological_space α] [has_le α] (s t : clopen_upper_set α) :
(s t) = s t
@[simp]
theorem clopen_upper_set.coe_inf {α : Type u_1} [topological_space α] [has_le α] (s t : clopen_upper_set α) :
(s t) = s t
@[simp]
theorem clopen_upper_set.coe_top {α : Type u_1} [topological_space α] [has_le α] :
@[simp]
theorem clopen_upper_set.coe_bot {α : Type u_1} [topological_space α] [has_le α] :
@[protected, instance]
Equations