mathlib3 documentation

topology.sets.order

Clopen upper sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

to_clopens : topological_space.clopens α
upper' : is_upper_set self.to_clopens.carrier

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} [topological_space α] [has_le α] :

set_like (clopen_upper_set α) α

Equations

clopen_upper_set.set_like = {coe := λ (s : clopen_upper_set α), s.to_clopens.carrier, coe_injective' := _}

theorem clopen_upper_set.upper {α : Type u_1} [topological_space α] [has_le α] (s : clopen_upper_set α) :

is_upper_set ↑s

theorem clopen_upper_set.clopen {α : Type u_1} [topological_space α] [has_le α] (s : clopen_upper_set α) :

@[simp]

theorem clopen_upper_set.to_upper_set_carrier {α : Type u_1} [topological_space α] [has_le α] (s : clopen_upper_set α) :

s.to_upper_set.carrier = ↑s

def clopen_upper_set.to_upper_set {α : Type u_1} [topological_space α] [has_le α] (s : clopen_upper_set α) :

Reinterpret a upper clopen as an upper set.

Equations

s.to_upper_set = {carrier := ↑s, upper' := _}

@[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]

def clopen_upper_set.has_sup {α : Type u_1} [topological_space α] [has_le α] :

has_sup (clopen_upper_set α)

Equations

clopen_upper_set.has_sup = {sup := λ (s t : clopen_upper_set α), {to_clopens := s.to_clopens ⊔ t.to_clopens, upper' := _}}

@[protected, instance]

def clopen_upper_set.has_inf {α : Type u_1} [topological_space α] [has_le α] :

has_inf (clopen_upper_set α)

Equations

clopen_upper_set.has_inf = {inf := λ (s t : clopen_upper_set α), {to_clopens := s.to_clopens ⊓ t.to_clopens, upper' := _}}

@[protected, instance]

def clopen_upper_set.has_top {α : Type u_1} [topological_space α] [has_le α] :

has_top (clopen_upper_set α)

Equations

clopen_upper_set.has_top = {top := {to_clopens := ⊤, upper' := _}}

@[protected, instance]

def clopen_upper_set.has_bot {α : Type u_1} [topological_space α] [has_le α] :

has_bot (clopen_upper_set α)

Equations

clopen_upper_set.has_bot = {bot := {to_clopens := ⊥, upper' := _}}

@[protected, instance]

def clopen_upper_set.lattice {α : Type u_1} [topological_space α] [has_le α] :

lattice (clopen_upper_set α)

Equations

clopen_upper_set.lattice = function.injective.lattice coe 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} [topological_space α] [has_le α] :

bounded_order (clopen_upper_set α)

Equations

clopen_upper_set.bounded_order = bounded_order.lift coe clopen_upper_set.bounded_order._proof_1 clopen_upper_set.bounded_order._proof_2 clopen_upper_set.bounded_order._proof_3

@[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 α] :

↑⊤ = set.univ

@[simp]

theorem clopen_upper_set.coe_bot {α : Type u_1} [topological_space α] [has_le α] :

@[protected, instance]

def clopen_upper_set.inhabited {α : Type u_1} [topological_space α] [has_le α] :

inhabited (clopen_upper_set α)

Equations

clopen_upper_set.inhabited = {default := ⊥}