# 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.

• carrier : Set α

the carrier set, i.e. the points in this set

• closed' : IsClosed self.carrier
Instances For
theorem TopologicalSpace.Closeds.closed' {α : Type u_4} [] (self : ) :
IsClosed self.carrier
Equations
• TopologicalSpace.Closeds.instSetLike = { coe := TopologicalSpace.Closeds.carrier, coe_injective' := }
instance TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed {α : Type u_2} [] :
CanLift (Set α) SetLike.coe IsClosed
Equations
• =
theorem TopologicalSpace.Closeds.closed {α : Type u_2} [] (s : ) :
def TopologicalSpace.Closeds.Simps.coe {α : Type u_2} [] (s : ) :
Set α

See Note [custom simps projection].

Equations
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
@[simp]
theorem TopologicalSpace.Closeds.coe_closure {α : Type u_2} [] (s : Set α) :
def TopologicalSpace.Closeds.closure {α : Type u_2} [] (s : Set α) :

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

Equations
• = { carrier := , closed' := }
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.

Equations
• TopologicalSpace.Closeds.gi = { choice := fun (s : Set α) (hs : ) => { carrier := s, closed' := }, gc := , le_l_u := , choice_eq := }
Instances For
Equations
• One or more equations did not get rendered due to their size.

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

Equations
• TopologicalSpace.Closeds.instInhabited = { default := }
@[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 =
theorem TopologicalSpace.Closeds.coe_nonempty {α : Type u_2} [] {s : } :
(s).Nonempty s
@[simp]
theorem TopologicalSpace.Closeds.coe_sInf {α : Type u_2} [] {S : } :
(sInf S) = iS, i
@[simp]
theorem TopologicalSpace.Closeds.coe_sSup {α : Type u_2} [] {S : } :
(sSup S) = closure (⋃₀ (SetLike.coe '' S))
@[simp]
theorem TopologicalSpace.Closeds.coe_finset_sup {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
(s.sup f) = s.sup (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Closeds.coe_finset_inf {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
(s.inf f) = s.inf (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Closeds.mem_sInf {α : Type u_2} [] {S : } {x : α} :
x sInf S sS, x 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' := }
@[simp]
theorem TopologicalSpace.Closeds.iInf_mk {α : Type u_2} [] {ι : Sort u_4} (s : ιSet α) (h : ∀ (i : ι), IsClosed (s i)) :
⨅ (i : ι), { carrier := s i, closed' := } = { carrier := ⋂ (i : ι), s i, closed' := }

Closed sets in a topological space form a coframe.

Equations
• TopologicalSpace.Closeds.coframeMinimalAxioms =
Instances For
Equations
@[simp]
theorem TopologicalSpace.Closeds.coe_singleton {α : Type u_2} [] [] (x : α) :
def TopologicalSpace.Closeds.singleton {α : Type u_2} [] [] (x : α) :

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

Equations
• = { carrier := {x}, closed' := }
Instances For
@[simp]
theorem TopologicalSpace.Closeds.mem_singleton {α : Type u_2} [] [] {a : α} {b : α} :
@[simp]
theorem TopologicalSpace.Closeds.compl_coe {α : Type u_2} [] (s : ) :
s.compl = (s)
def TopologicalSpace.Closeds.compl {α : Type u_2} [] (s : ) :

The complement of a closed set as an open set.

Equations
• s.compl = { carrier := (s), is_open' := }
Instances For
@[simp]
theorem TopologicalSpace.Opens.coe_compl {α : Type u_2} [] (s : ) :
s.compl = (s)
def TopologicalSpace.Opens.compl {α : Type u_2} [] (s : ) :

The complement of an open set as a closed set.

Equations
• s.compl = { carrier := (s), closed' := }
Instances For
theorem TopologicalSpace.Closeds.compl_compl {α : Type u_2} [] (s : ) :
s.compl.compl = s
theorem TopologicalSpace.Opens.compl_compl {α : Type u_2} [] (s : ) :
s.compl.compl = 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_apply (α : Type u_2) [] :
∀ (a : ), = (OrderDual.toDual TopologicalSpace.Closeds.compl) a
@[simp]
theorem TopologicalSpace.Closeds.complOrderIso_symm_apply (α : Type u_2) [] :
∀ (a : ), = (TopologicalSpace.Opens.compl OrderDual.ofDual) a

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopologicalSpace.Opens.complOrderIso_apply (α : Type u_2) [] :
∀ (a : ), = (OrderDual.toDual TopologicalSpace.Opens.compl) a
@[simp]
theorem TopologicalSpace.Opens.complOrderIso_symm_apply (α : Type u_2) [] :
∀ (a : ), = (TopologicalSpace.Closeds.compl OrderDual.ofDual) a

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopologicalSpace.Closeds.coe_eq_singleton_of_isAtom {α : Type u_2} [] [] {s : } (hs : ) :
∃ (a : α), s = {a}
@[simp]
theorem TopologicalSpace.Closeds.isAtom_coe {α : Type u_2} [] [] {s : } :
IsAtom s
theorem TopologicalSpace.Closeds.isAtom_iff {α : Type u_2} [] [] {s : } :
∃ (x : α),

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

theorem TopologicalSpace.Opens.isCoatom_iff {α : Type u_2} [] [] {s : } :
∃ (x : α), s = .compl

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.

• carrier : Set α

the carrier set, i.e. the points in this set

• isClopen' : IsClopen self.carrier
Instances For
theorem TopologicalSpace.Clopens.isClopen' {α : Type u_4} [] (self : ) :
IsClopen self.carrier
Equations
• TopologicalSpace.Clopens.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }
theorem TopologicalSpace.Clopens.isClopen {α : Type u_2} [] (s : ) :
def TopologicalSpace.Clopens.Simps.coe {α : Type u_2} [] (s : ) :
Set α

See Note [custom simps projection].

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

Reinterpret a clopen as an open.

Equations
• s.toOpens = { carrier := s, is_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, isClopen' := h } = s
@[simp]
theorem TopologicalSpace.Clopens.mem_mk {α : Type u_2} [] {s : Set α} {x : α} {h : } :
x { carrier := s, isClopen' := h } x s
instance TopologicalSpace.Clopens.instSup {α : Type u_2} [] :
Equations
• TopologicalSpace.Clopens.instSup = { sup := fun (s t : ) => { carrier := s t, isClopen' := } }
instance TopologicalSpace.Clopens.instInf {α : Type u_2} [] :
Equations
• TopologicalSpace.Clopens.instInf = { inf := fun (s t : ) => { carrier := s t, isClopen' := } }
instance TopologicalSpace.Clopens.instTop {α : Type u_2} [] :
Equations
• TopologicalSpace.Clopens.instTop = { top := { carrier := , isClopen' := } }
instance TopologicalSpace.Clopens.instBot {α : Type u_2} [] :
Equations
• TopologicalSpace.Clopens.instBot = { bot := { carrier := , isClopen' := } }
instance TopologicalSpace.Clopens.instSDiff {α : Type u_2} [] :
Equations
• TopologicalSpace.Clopens.instSDiff = { sdiff := fun (s t : ) => { carrier := s \ t, isClopen' := } }
instance TopologicalSpace.Clopens.instHImp {α : Type u_2} [] :
Equations
• TopologicalSpace.Clopens.instHImp = { himp := fun (s t : ) => { carrier := s t, isClopen' := } }
Equations
• TopologicalSpace.Clopens.instHasCompl = { compl := fun (s : ) => { carrier := (s), isClopen' := } }
@[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_himp {α : Type u_2} [] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem TopologicalSpace.Clopens.coe_compl {α : Type u_2} [] (s : ) :
s = (s)
Equations
Equations
• TopologicalSpace.Clopens.instInhabited = { default := }
instance TopologicalSpace.Clopens.instSProdProd {α : Type u_2} {β : Type u_3} [] [] :
Equations
• TopologicalSpace.Clopens.instSProdProd = { sprod := fun (s : ) (t : ) => { carrier := s ×ˢ t, isClopen' := } }
@[simp]
theorem TopologicalSpace.Clopens.mem_prod {α : Type u_2} {β : Type u_3} [] [] {s : } {t : } {x : α × β} :
x s ×ˢ t x.1 s x.2 t

### Irreducible closed sets #

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

The type of irreducible closed subsets of a topological space.

• carrier : Set α

the carrier set, i.e. the points in this set

• is_irreducible' : IsIrreducible self.carrier
• is_closed' : IsClosed self.carrier
Instances For
theorem TopologicalSpace.IrreducibleCloseds.is_closed' {α : Type u_4} [] (self : ) :
IsClosed self.carrier
Equations
• TopologicalSpace.IrreducibleCloseds.instSetLike = { coe := TopologicalSpace.IrreducibleCloseds.carrier, coe_injective' := }
Equations
• =

See Note [custom simps projection].

Equations
Instances For
theorem TopologicalSpace.IrreducibleCloseds.ext {α : Type u_2} [] (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.coe_mk {α : Type u_2} [] (s : Set α) (h : ) (h' : ) :
{ carrier := s, is_irreducible' := h, is_closed' := h' } = s
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.coe_singleton {α : Type u_2} [] [] (x : α) :
def TopologicalSpace.IrreducibleCloseds.singleton {α : Type u_2} [] [] (x : α) :

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

Equations
• = { carrier := {x}, is_irreducible' := , is_closed' := }
Instances For
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.mem_singleton {α : Type u_2} [] [] {a : α} {b : α} :
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.equivSubtype_apply {α : Type u_2} [] :
TopologicalSpace.IrreducibleCloseds.equivSubtype a = a.carrier,
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply {α : Type u_2} [] (a : { x : Set α // }) :
TopologicalSpace.IrreducibleCloseds.equivSubtype.symm a = { carrier := a, is_irreducible' := , is_closed' := }

The equivalence between IrreducibleCloseds α and {x : Set α // IsIrreducible x ∧ IsClosed x }.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply {α : Type u_2} [] (a : { x : Set α // }) :
TopologicalSpace.IrreducibleCloseds.equivSubtype'.symm a = { carrier := a, is_irreducible' := , is_closed' := }
@[simp]
theorem TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply {α : Type u_2} [] :
TopologicalSpace.IrreducibleCloseds.equivSubtype' a = a.carrier,

The equivalence between IrreducibleCloseds α and {x : Set α // IsClosed x ∧ IsIrreducible x }.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The equivalence IrreducibleCloseds α ≃ { x : Set α // IsIrreducible x ∧ IsClosed x } is an order isomorphism.

Equations
• = TopologicalSpace.IrreducibleCloseds.equivSubtype.toOrderIso
Instances For

The equivalence IrreducibleCloseds α ≃ { x : Set α // IsClosed x ∧ IsIrreducible x } is an order isomorphism.

Equations
• = TopologicalSpace.IrreducibleCloseds.equivSubtype'.toOrderIso
Instances For