mathlib documentation

topology.sets.order

Clopen upper sets #

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

Compact open sets #

@[protected, instance]
Equations

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]
@[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]
@[simp]
@[protected, instance]
Equations