# Documentation

Mathlib.Topology.Sets.Closeds

# Closed sets #

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

## Main Definitions #

For a topological space α,

• TopologicalSpace.Closeds α: The type of closed sets.
• TopologicalSpace.Clopens α: The type of clopen sets.

### Closed sets #

structure TopologicalSpace.Closeds (α : Type u_4) [] :
Type u_4

The type of closed subsets of a topological space.

Instances For
theorem TopologicalSpace.Closeds.closed {α : Type u_2} [] (s : ) :
def TopologicalSpace.Closeds.Simps.coe {α : Type u_2} [] (s : ) :
Set α

See Note [custom simps projection].

Instances For
theorem TopologicalSpace.Closeds.ext {α : Type u_2} [] {s : } {t : } (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.Closeds.coe_mk {α : Type u_2} [] (s : Set α) (h : ) :
{ carrier := s, closed' := h } = s
def TopologicalSpace.Closeds.closure {α : Type u_2} [] (s : Set α) :

The closure of a set, as an element of TopologicalSpace.Closeds.

Instances For
theorem TopologicalSpace.Closeds.gc {α : Type u_2} [] :
GaloisConnection TopologicalSpace.Closeds.closure SetLike.coe
def TopologicalSpace.Closeds.gi {α : Type u_2} [] :
GaloisInsertion TopologicalSpace.Closeds.closure SetLike.coe

The galois coinsertion between sets and opens.

Instances For

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

@[simp]
theorem TopologicalSpace.Closeds.coe_sup {α : Type u_2} [] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem TopologicalSpace.Closeds.coe_inf {α : Type u_2} [] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem TopologicalSpace.Closeds.coe_top {α : Type u_2} [] :
= Set.univ
@[simp]
theorem TopologicalSpace.Closeds.coe_eq_univ {α : Type u_2} [] {s : } :
s = Set.univ s =
@[simp]
theorem TopologicalSpace.Closeds.coe_bot {α : Type u_2} [] :
=
@[simp]
theorem TopologicalSpace.Closeds.coe_eq_empty {α : Type u_2} [] {s : } :
s = s =
@[simp]
theorem TopologicalSpace.Closeds.coe_sInf {α : Type u_2} [] {S : } :
↑(sInf S) = ⋂ (i : ) (_ : i S), i
@[simp]
theorem TopologicalSpace.Closeds.coe_finset_sup {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
↑() = Finset.sup s (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Closeds.coe_finset_inf {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
↑() = Finset.inf s (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Closeds.mem_sInf {α : Type u_2} [] {S : } {x : α} :
x sInf S ∀ (s : ), s Sx s
@[simp]
theorem TopologicalSpace.Closeds.mem_iInf {α : Type u_2} [] {ι : Sort u_4} {x : α} {s : } :
x iInf s ∀ (i : ι), x s i
@[simp]
theorem TopologicalSpace.Closeds.coe_iInf {α : Type u_2} [] {ι : Sort u_4} (s : ) :
↑(⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)
theorem TopologicalSpace.Closeds.iInf_def {α : Type u_2} [] {ι : Sort u_4} (s : ) :
⨅ (i : ι), s i = { carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }
@[simp]
theorem TopologicalSpace.Closeds.iInf_mk {α : Type u_2} [] {ι : Sort u_4} (s : ιSet α) (h : ∀ (i : ι), IsClosed (s i)) :
⨅ (i : ι), { carrier := s i, closed' := h i } = { carrier := ⋂ (i : ι), s i, closed' := (_ : IsClosed (⋂ (i : ι), s i)) }
@[simp]
theorem TopologicalSpace.Closeds.singleton_coe {α : Type u_2} [] [] (x : α) :
def TopologicalSpace.Closeds.singleton {α : Type u_2} [] [] (x : α) :

The term of TopologicalSpace.Closeds α corresponding to a singleton.

Instances For
@[simp]
theorem TopologicalSpace.Closeds.compl_coe {α : Type u_2} [] (s : ) :
= (s)
def TopologicalSpace.Closeds.compl {α : Type u_2} [] (s : ) :

The complement of a closed set as an open set.

Instances For
@[simp]
theorem TopologicalSpace.Opens.compl_coe {α : Type u_2} [] (s : ) :
= (s)
def TopologicalSpace.Opens.compl {α : Type u_2} [] (s : ) :

The complement of an open set as a closed set.

Instances For
theorem TopologicalSpace.Closeds.compl_compl {α : Type u_2} [] (s : ) :
theorem TopologicalSpace.Opens.compl_compl {α : Type u_2} [] (s : ) :
theorem TopologicalSpace.Closeds.compl_bijective {α : Type u_2} [] :
Function.Bijective TopologicalSpace.Closeds.compl
theorem TopologicalSpace.Opens.compl_bijective {α : Type u_2} [] :
Function.Bijective TopologicalSpace.Opens.compl
@[simp]
theorem TopologicalSpace.Closeds.complOrderIso_symm_apply (α : Type u_2) [] :
∀ (a : ), = (TopologicalSpace.Opens.compl OrderDual.ofDual) a
@[simp]
theorem TopologicalSpace.Closeds.complOrderIso_apply (α : Type u_2) [] :
∀ (a : ), = (OrderDual.toDual TopologicalSpace.Closeds.compl) a

TopologicalSpace.Closeds.compl as an OrderIso to the order dual of TopologicalSpace.Opens α.

Instances For
@[simp]
theorem TopologicalSpace.Opens.complOrderIso_symm_apply (α : Type u_2) [] :
∀ (a : ), = (TopologicalSpace.Closeds.compl OrderDual.ofDual) a
@[simp]
theorem TopologicalSpace.Opens.complOrderIso_apply (α : Type u_2) [] :
∀ (a : ), = (OrderDual.toDual TopologicalSpace.Opens.compl) a

TopologicalSpace.Opens.compl as an OrderIso to the order dual of TopologicalSpace.Closeds α.

Instances For
theorem TopologicalSpace.Closeds.isAtom_iff {α : Type u_2} [] [] {s : } :

in a T1Space, atoms of TopologicalSpace.Closeds α are precisely the TopologicalSpace.Closeds.singletons.

TODO: use minimal_nonempty_closed_eq_singleton to show that an atom in TopologicalSpace.Closeds in a T₀ space is a singleton.

theorem TopologicalSpace.Opens.isCoatom_iff {α : Type u_2} [] [] {s : } :

in a T1Space, coatoms of TopologicalSpace.Opens α are precisely complements of singletons: (TopologicalSpace.Closeds.singleton x).compl.

### Clopen sets #

structure TopologicalSpace.Clopens (α : Type u_4) [] :
Type u_4

The type of clopen sets of a topological space.

Instances For
theorem TopologicalSpace.Clopens.clopen {α : Type u_2} [] (s : ) :
def TopologicalSpace.Clopens.Simps.coe {α : Type u_2} [] (s : ) :
Set α

See Note [custom simps projection].

Instances For
@[simp]
theorem TopologicalSpace.Clopens.toOpens_coe {α : Type u_2} [] (s : ) :
def TopologicalSpace.Clopens.toOpens {α : Type u_2} [] (s : ) :

Reinterpret a clopen as an open.

Instances For
theorem TopologicalSpace.Clopens.ext {α : Type u_2} [] {s : } {t : } (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.Clopens.coe_mk {α : Type u_2} [] (s : Set α) (h : ) :
{ carrier := s, clopen' := h } = s
@[simp]
theorem TopologicalSpace.Clopens.coe_sup {α : Type u_2} [] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem TopologicalSpace.Clopens.coe_inf {α : Type u_2} [] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem TopologicalSpace.Clopens.coe_top {α : Type u_2} [] :
= Set.univ
@[simp]
theorem TopologicalSpace.Clopens.coe_bot {α : Type u_2} [] :
=
@[simp]
theorem TopologicalSpace.Clopens.coe_sdiff {α : Type u_2} [] (s : ) (t : ) :
↑(s \ t) = s \ t
@[simp]
theorem TopologicalSpace.Clopens.coe_compl {α : Type u_2} [] (s : ) :
s = (s)