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 #

source
structure topological_space.closeds (α : Type u_3) [topological_space α] :
Type u_3

The type of closed subsets of a topological space.

source
@[protected, instance]
def topological_space.closeds.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.closeds α) α
Equations
source
theorem topological_space.closeds.closed {α : Type u_1} [topological_space α] (s : topological_space.closeds α) :
is_closed ↑s
source
@[protected, ext]
theorem topological_space.closeds.ext {α : Type u_1} [topological_space α] {s t : topological_space.closeds α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.closeds.coe_mk {α : Type u_1} [topological_space α] (s : set α) (h : is_closed s) :
↑{carrier := s, closed' := h} = s
source
@[protected, instance]
def topological_space.closeds.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.closeds α)
Equations
source
@[protected, instance]
def topological_space.closeds.has_inf {α : Type u_1} [topological_space α] :
has_inf (topological_space.closeds α)
Equations
source
@[protected, instance]
def topological_space.closeds.has_top {α : Type u_1} [topological_space α] :
has_top (topological_space.closeds α)
Equations
source
@[protected, instance]
def topological_space.closeds.has_bot {α : Type u_1} [topological_space α] :
has_bot (topological_space.closeds α)
Equations
source
@[protected, instance]
def topological_space.closeds.distrib_lattice {α : Type u_1} [topological_space α] :
distrib_lattice (topological_space.closeds α)
Equations
source
@[protected, instance]
def topological_space.closeds.bounded_order {α : Type u_1} [topological_space α] :
bounded_order (topological_space.closeds α)
Equations
source
@[protected, instance]
def topological_space.closeds.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.closeds α)

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

Equations
source
@[simp]
theorem topological_space.closeds.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.closeds α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.closeds.coe_inf {α : Type u_1} [topological_space α] (s t : topological_space.closeds α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem topological_space.closeds.coe_top {α : Type u_1} [topological_space α] :
↑⊤ = set.univ
source
@[simp]
theorem topological_space.closeds.coe_bot {α : Type u_1} [topological_space α] :
↑⊥ = ∅

Clopen sets #

source
structure topological_space.clopens (α : Type u_3) [topological_space α] :
Type u_3

The type of clopen sets of a topological space.

source
@[protected, instance]
def topological_space.clopens.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.clopens α) α
Equations
source
theorem topological_space.clopens.clopen {α : Type u_1} [topological_space α] (s : topological_space.clopens α) :
is_clopen ↑s
source
@[simp]
theorem topological_space.clopens.to_opens_coe {α : Type u_1} [topological_space α] (s : topological_space.clopens α) :
↑(s.to_opens) = ↑s
source
def topological_space.clopens.to_opens {α : Type u_1} [topological_space α] (s : topological_space.clopens α) :
topological_space.opens α

Reinterpret a compact open as an open.

Equations
source
@[protected, ext]
theorem topological_space.clopens.ext {α : Type u_1} [topological_space α] {s t : topological_space.clopens α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.clopens.coe_mk {α : Type u_1} [topological_space α] (s : set α) (h : is_clopen s) :
↑{carrier := s, clopen' := h} = s
source
@[protected, instance]
def topological_space.clopens.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.clopens α)
Equations
source
@[protected, instance]
def topological_space.clopens.has_inf {α : Type u_1} [topological_space α] :
has_inf (topological_space.clopens α)
Equations
source
@[protected, instance]
def topological_space.clopens.has_top {α : Type u_1} [topological_space α] :
has_top (topological_space.clopens α)
Equations
source
@[protected, instance]
def topological_space.clopens.has_bot {α : Type u_1} [topological_space α] :
has_bot (topological_space.clopens α)
Equations
source
@[protected, instance]
def topological_space.clopens.has_sdiff {α : Type u_1} [topological_space α] :
has_sdiff (topological_space.clopens α)
Equations
source
@[protected, instance]
def topological_space.clopens.has_compl {α : Type u_1} [topological_space α] :
has_compl (topological_space.clopens α)
Equations
source
@[protected, instance]
def topological_space.clopens.boolean_algebra {α : Type u_1} [topological_space α] :
boolean_algebra (topological_space.clopens α)
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
source
@[simp]
theorem topological_space.clopens.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.clopens α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.clopens.coe_inf {α : Type u_1} [topological_space α] (s t : topological_space.clopens α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem topological_space.clopens.coe_top {α : Type u_1} [topological_space α] :
↑⊤ = set.univ
source
@[simp]
theorem topological_space.clopens.coe_bot {α : Type u_1} [topological_space α] :
↑⊥ = ∅
source
@[simp]
theorem topological_space.clopens.coe_sdiff {α : Type u_1} [topological_space α] (s t : topological_space.clopens α) :
↑(s \ t) = ↑s \ ↑t
source
@[simp]
theorem topological_space.clopens.coe_compl {α : Type u_1} [topological_space α] (s : topological_space.clopens α) :
↑sᶜ = (↑s)ᶜ
source
@[protected, instance]
def topological_space.clopens.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.clopens α)
Equations