mathlib documentation

topology.sets.closeds

Closed sets #

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
@[simp]
theorem topological_space.closeds.mem_Inf {α : Type u_2} [topological_space α] {S : set (topological_space.closeds α)} {x : α} :
x has_Inf.Inf S ∀ (s : topological_space.closeds α), s Sx s

The complement of a closed set as an open set.

Equations

The complement of an open set as a closed set.

Equations

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
@[simp]
@[simp]
@[simp]
@[simp]
theorem topological_space.clopens.coe_sdiff {α : Type u_2} [topological_space α] (s t : topological_space.clopens α) :
(s \ t) = s \ t