# mathlib3documentation

topology.sets.closeds

# Closed sets #

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

We define a few types of closed sets in a topological space.

## Main Definitions #

For a topological space α,

• closeds α: The type of closed sets.
• clopens α: The type of clopen sets.

### Closed sets #

structure topological_space.closeds (α : Type u_4)  :
Type u_4

The type of closed subsets of a topological space.

Instances for topological_space.closeds
@[protected, instance]
Equations
@[protected, ext]
theorem topological_space.closeds.ext {α : Type u_2} {s t : topological_space.closeds α} (h : s = t) :
s = t
@[simp]
theorem topological_space.closeds.coe_mk {α : Type u_2} (s : set α) (h : is_closed s) :
{carrier := s, closed' := h} = s
@[protected]
def topological_space.closeds.closure {α : Type u_2} (s : set α) :

The closure of a set, as an element of closeds.

Equations

The galois coinsertion between sets and opens.

Equations
@[protected, instance]
Equations
@[protected, instance]

The type of closed sets is inhabited, with default element the empty set.

Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem topological_space.closeds.coe_top {α : Type u_2}  :
@[simp, norm_cast]
theorem topological_space.closeds.coe_bot {α : Type u_2}  :
@[simp, norm_cast]
theorem topological_space.closeds.coe_Inf {α : Type u_2} {S : set } :
(has_Inf.Inf S) = (i : (H : i S), i
@[simp, norm_cast]
theorem topological_space.closeds.coe_finset_sup {ι : Type u_1} {α : Type u_2} (f : ι ) (s : finset ι) :
(s.sup f) = s.sup (coe f)
@[simp, norm_cast]
theorem topological_space.closeds.coe_finset_inf {ι : Type u_1} {α : Type u_2} (f : ι ) (s : finset ι) :
(s.inf f) = s.inf (coe f)
theorem topological_space.closeds.infi_def {α : Type u_2} {ι : Sort u_1} (s : ι ) :
( (i : ι), s i) = {carrier := (i : ι), (s i), closed' := _}
@[simp]
theorem topological_space.closeds.infi_mk {α : Type u_2} {ι : Sort u_1} (s : ι set α) (h : (i : ι), is_closed (s i)) :
( (i : ι), {carrier := s i, closed' := _}) = {carrier := (i : ι), s i, closed' := _}
@[simp, norm_cast]
theorem topological_space.closeds.coe_infi {α : Type u_2} {ι : Sort u_1} (s : ι ) :
( (i : ι), s i) = (i : ι), (s i)
@[simp]
theorem topological_space.closeds.mem_infi {α : Type u_2} {ι : Sort u_1} {x : α} {s : ι } :
x infi s (i : ι), x s i
@[simp]
theorem topological_space.closeds.mem_Inf {α : Type u_2} {S : set } {x : α} :
x (s : , s S x s
@[protected, instance]
Equations
@[simp]
theorem topological_space.closeds.singleton_carrier {α : Type u_2} [t1_space α] (x : α) :
def topological_space.closeds.singleton {α : Type u_2} [t1_space α] (x : α) :

The term of closeds α corresponding to a singleton.

Equations
@[simp]
theorem topological_space.closeds.compl_coe {α : Type u_2}  :

The complement of a closed set as an open set.

Equations

The complement of an open set as a closed set.

Equations
@[simp]

closeds.compl as an order_iso to the order dual of opens α.

Equations
@[simp]
@[simp]

opens.compl as an order_iso to the order dual of closeds α.

Equations
@[simp]
theorem topological_space.closeds.is_atom_iff {α : Type u_2} [t1_space α]  :
(x : α),

in a t1_space, atoms of closeds α are precisely the closeds.singletons.

in a t1_space, coatoms of opens α are precisely complements of singletons: (closeds.singleton x).compl.

### Clopen sets #

structure topological_space.clopens (α : Type u_4)  :
Type u_4

The type of clopen sets of a topological space.

Instances for topological_space.clopens
@[protected, instance]
Equations
@[simp]

Reinterpret a compact open as an open.

Equations
@[protected, ext]
theorem topological_space.clopens.ext {α : Type u_2} {s t : topological_space.clopens α} (h : s = t) :
s = t
@[simp]
theorem topological_space.clopens.coe_mk {α : Type u_2} (s : set α) (h : is_clopen s) :
{carrier := s, clopen' := h} = s
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
• topological_space.clopens.boolean_algebra = topological_space.clopens.boolean_algebra._proof_1 topological_space.clopens.boolean_algebra._proof_2 topological_space.clopens.boolean_algebra._proof_3 topological_space.clopens.boolean_algebra._proof_4 topological_space.clopens.boolean_algebra._proof_5 topological_space.clopens.boolean_algebra._proof_6 topological_space.clopens.boolean_algebra._proof_7
@[simp]
@[simp]
@[simp]
theorem topological_space.clopens.coe_top {α : Type u_2}  :
@[simp]
theorem topological_space.clopens.coe_bot {α : Type u_2}  :
@[simp]
@[simp]
@[protected, instance]
Equations