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 #

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

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

Equations
@[simp]
@[simp]
@[simp]

Clopen sets #

Reinterpret a compact open as an open.

Equations
@[protected, ext]
theorem topological_space.clopens.ext {α : Type u_1} [topological_space α] {s t : topological_space.clopens α} (h : s = t) :
s = t
@[simp]
theorem topological_space.clopens.coe_mk {α : Type u_1} [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_1} [topological_space α] (s t : topological_space.clopens α) :
(s \ t) = s \ t