mathlib3 documentation

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 α,

Closed sets #

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

The type of closed subsets of a topological space.

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

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]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem topological_space.closeds.coe_finset_sup {ι : Type u_1} {α : Type u_2} [topological_space α] (f : ι topological_space.closeds α) (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} [topological_space α] (f : ι topological_space.closeds α) (s : finset ι) :
(s.inf f) = s.inf (coe f)
theorem topological_space.closeds.infi_def {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι topological_space.closeds α) :
( (i : ι), s i) = {carrier := (i : ι), (s i), closed' := _}
@[simp]
theorem topological_space.closeds.infi_mk {α : Type u_2} [topological_space α] {ι : 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} [topological_space α] {ι : Sort u_1} (s : ι topological_space.closeds α) :
( (i : ι), s i) = (i : ι), (s i)
@[simp]
theorem topological_space.closeds.mem_infi {α : Type u_2} [topological_space α] {ι : Sort u_1} {x : α} {s : ι topological_space.closeds α} :
x infi s (i : ι), x s i

The term of closeds α corresponding to a singleton.

Equations

The complement of a closed set as an open set.

Equations

The complement of an open set as a closed set.

Equations

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 #

Reinterpret a compact open as an open.

Equations
@[protected, ext]
theorem topological_space.clopens.ext {α : Type u_2} [topological_space α] {s t : topological_space.clopens α} (h : s = t) :
s = t
@[simp]
theorem topological_space.clopens.coe_mk {α : Type u_2} [topological_space α] (s : set α) (h : is_clopen s) :
{carrier := s, clopen' := h} = s
@[protected, instance]
Equations
  • topological_space.clopens.boolean_algebra = function.injective.boolean_algebra coe 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