mathlib documentation

topology.sets.compacts

Compact sets #

We define a few types of compact sets in a topological space.

Main Definitions #

For a topological space α,

Compact sets #

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

The type of compact sets of a topological space.

source
@[protected, instance]
def topological_space.compacts.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.compacts α) α
Equations
source
theorem topological_space.compacts.compact {α : Type u_1} [topological_space α] (s : topological_space.compacts α) :
is_compact ↑s
source
@[protected, instance]
def topological_space.compacts.compact_space {α : Type u_1} [topological_space α] (K : topological_space.compacts α) :
compact_space ↥K
source
@[protected, instance]
def topological_space.compacts.can_lift {α : Type u_1} [topological_space α] :
can_lift (set α) (topological_space.compacts α)
Equations
source
@[protected, ext]
theorem topological_space.compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.compacts α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.compacts.coe_mk {α : Type u_1} [topological_space α] (s : set α) (h : is_compact s) :
↑{carrier := s, compact' := h} = s
source
@[protected, instance]
def topological_space.compacts.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.has_inf {α : Type u_1} [topological_space α] [t2_space α] :
has_inf (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.has_top {α : Type u_1} [topological_space α] [compact_space α] :
has_top (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.has_bot {α : Type u_1} [topological_space α] :
has_bot (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.distrib_lattice {α : Type u_1} [topological_space α] [t2_space α] :
distrib_lattice (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.order_bot {α : Type u_1} [topological_space α] :
order_bot (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.bounded_order {α : Type u_1} [topological_space α] [compact_space α] :
bounded_order (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.compacts α)

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

Equations
source
@[simp]
theorem topological_space.compacts.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.compacts α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.compacts.coe_inf {α : Type u_1} [topological_space α] [t2_space α] (s t : topological_space.compacts α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem topological_space.compacts.coe_top {α : Type u_1} [topological_space α] [compact_space α] :
↑⊤ = set.univ
source
@[simp]
theorem topological_space.compacts.coe_bot {α : Type u_1} [topological_space α] :
↑⊥ = ∅
source
@[simp]
theorem topological_space.compacts.coe_finset_sup {α : Type u_1} [topological_space α] {ι : Type u_2} {s : finset ι} {f : ι → topological_space.compacts α} :
↑(s.sup f) = s.sup (λ (i : ι), ↑(f i))
source
@[protected]
def topological_space.compacts.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (K : topological_space.compacts α) :
topological_space.compacts β

The image of a compact set under a continuous function.

Equations
source
@[simp]
theorem topological_space.compacts.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (s : topological_space.compacts α) :
↑(topological_space.compacts.map f hf s) = f '' ↑s
source
@[protected, simp]
def topological_space.compacts.equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
topological_space.compacts α ≃ topological_space.compacts β

A homeomorphism induces an equivalence on compact sets, by taking the image.

Equations
source
theorem topological_space.compacts.equiv_to_fun_val {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) (K : topological_space.compacts α) :
(⇑(topological_space.compacts.equiv f) K).carrier = ⇑(f.symm) ⁻¹' K.carrier

The image of a compact set under a homeomorphism can also be expressed as a preimage.

Nonempty compact sets #

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

The type of nonempty compact sets of a topological space.

source
@[protected, instance]
def topological_space.nonempty_compacts.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.nonempty_compacts α) α
Equations
source
theorem topological_space.nonempty_compacts.compact {α : Type u_1} [topological_space α] (s : topological_space.nonempty_compacts α) :
is_compact ↑s
source
@[protected]
theorem topological_space.nonempty_compacts.nonempty {α : Type u_1} [topological_space α] (s : topological_space.nonempty_compacts α) :
↑s.nonempty
source
def topological_space.nonempty_compacts.to_closeds {α : Type u_1} [topological_space α] [t2_space α] (s : topological_space.nonempty_compacts α) :
topological_space.closeds α

Reinterpret a nonempty compact as a closed set.

Equations
source
@[protected, ext]
theorem topological_space.nonempty_compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.nonempty_compacts α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.nonempty_compacts.coe_mk {α : Type u_1} [topological_space α] (s : topological_space.compacts α) (h : s.carrier.nonempty) :
↑{to_compacts := s, nonempty' := h} = ↑s
source
@[protected, instance]
def topological_space.nonempty_compacts.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.nonempty_compacts α)
Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.has_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
has_top (topological_space.nonempty_compacts α)
Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.nonempty_compacts α)
Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.order_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
order_top (topological_space.nonempty_compacts α)
Equations
source
@[simp]
theorem topological_space.nonempty_compacts.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.nonempty_compacts α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.nonempty_compacts.coe_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
↑⊤ = set.univ
source
@[protected, instance]
def topological_space.nonempty_compacts.inhabited {α : Type u_1} [topological_space α] [inhabited α] :
inhabited (topological_space.nonempty_compacts α)

In an inhabited space, the type of nonempty compact subsets is also inhabited, with default element the singleton set containing the default element.

Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.to_compact_space {α : Type u_1} [topological_space α] {s : topological_space.nonempty_compacts α} :
compact_space ↥s
source
@[protected, instance]
def topological_space.nonempty_compacts.to_nonempty {α : Type u_1} [topological_space α] {s : topological_space.nonempty_compacts α} :
nonempty ↥s

Positive compact sets #

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

The type of compact sets nonempty interior of a topological space. See also compacts and nonempty_compacts

source
@[protected, instance]
def topological_space.positive_compacts.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.positive_compacts α) α
Equations
source
theorem topological_space.positive_compacts.compact {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
is_compact ↑s
source
theorem topological_space.positive_compacts.interior_nonempty {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
(interior ↑s).nonempty
source
def topological_space.positive_compacts.to_nonempty_compacts {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
topological_space.nonempty_compacts α

Reinterpret a positive compact as a nonempty compact.

Equations
source
@[protected, ext]
theorem topological_space.positive_compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.positive_compacts α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.positive_compacts.coe_mk {α : Type u_1} [topological_space α] (s : topological_space.compacts α) (h : (interior s.carrier).nonempty) :
↑{to_compacts := s, interior_nonempty' := h} = ↑s
source
@[protected, instance]
def topological_space.positive_compacts.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.has_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
has_top (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.order_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
order_top (topological_space.positive_compacts α)
Equations
source
@[simp]
theorem topological_space.positive_compacts.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.positive_compacts α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.positive_compacts.coe_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
↑⊤ = set.univ
source
@[protected, instance]
def topological_space.positive_compacts.inhabited {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
inhabited (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.nonempty {α : Type u_1} [topological_space α] [locally_compact_space α] [nonempty α] :
nonempty (topological_space.positive_compacts α)

In a nonempty locally compact space, there exists a compact set with nonempty interior.

Compact open sets #

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

The type of compact open sets of a topological space. This is useful in non Hausdorff contexts, in particular spectral spaces.

source
@[protected, instance]
def topological_space.compact_opens.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.compact_opens α) α
Equations
source
theorem topological_space.compact_opens.compact {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
is_compact ↑s
source
theorem topological_space.compact_opens.open {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
is_open ↑s
source
def topological_space.compact_opens.to_opens {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
topological_space.opens α

Reinterpret a compact open as an open.

Equations
source
@[simp]
theorem topological_space.compact_opens.to_opens_coe {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
↑(s.to_opens) = ↑s
source
@[simp]
theorem topological_space.compact_opens.to_clopens_carrier {α : Type u_1} [topological_space α] [t2_space α] (s : topological_space.compact_opens α) :
s.to_clopens.carrier = ↑s
source
def topological_space.compact_opens.to_clopens {α : Type u_1} [topological_space α] [t2_space α] (s : topological_space.compact_opens α) :
topological_space.clopens α

Reinterpret a compact open as a clopen.

Equations
source
@[protected, ext]
theorem topological_space.compact_opens.ext {α : Type u_1} [topological_space α] {s t : topological_space.compact_opens α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.compact_opens.coe_mk {α : Type u_1} [topological_space α] (s : topological_space.compacts α) (h : is_open s.carrier) :
↑{to_compacts := s, open' := h} = ↑s
source
@[protected, instance]
def topological_space.compact_opens.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_inf {α : Type u_1} [topological_space α] [t2_space α] :
has_inf (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_top {α : Type u_1} [topological_space α] [compact_space α] :
has_top (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_bot {α : Type u_1} [topological_space α] :
has_bot (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_sdiff {α : Type u_1} [topological_space α] [t2_space α] :
has_sdiff (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_compl {α : Type u_1} [topological_space α] [t2_space α] [compact_space α] :
has_compl (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.order_bot {α : Type u_1} [topological_space α] :
order_bot (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.generalized_boolean_algebra {α : Type u_1} [topological_space α] [t2_space α] :
generalized_boolean_algebra (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.bounded_order {α : Type u_1} [topological_space α] [compact_space α] :
bounded_order (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.boolean_algebra {α : Type u_1} [topological_space α] [t2_space α] [compact_space α] :
boolean_algebra (topological_space.compact_opens α)
Equations
  • topological_space.compact_opens.boolean_algebra = function.injective.boolean_algebra coe topological_space.compact_opens.boolean_algebra._proof_1 topological_space.compact_opens.boolean_algebra._proof_2 topological_space.compact_opens.boolean_algebra._proof_3 topological_space.compact_opens.boolean_algebra._proof_4 topological_space.compact_opens.boolean_algebra._proof_5 topological_space.compact_opens.boolean_algebra._proof_6 topological_space.compact_opens.boolean_algebra._proof_7
source
@[simp]
theorem topological_space.compact_opens.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.compact_opens α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.compact_opens.coe_inf {α : Type u_1} [topological_space α] [t2_space α] (s t : topological_space.compact_opens α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem topological_space.compact_opens.coe_top {α : Type u_1} [topological_space α] [compact_space α] :
↑⊤ = set.univ
source
@[simp]
theorem topological_space.compact_opens.coe_bot {α : Type u_1} [topological_space α] :
↑⊥ = ∅
source
@[simp]
theorem topological_space.compact_opens.coe_sdiff {α : Type u_1} [topological_space α] [t2_space α] (s t : topological_space.compact_opens α) :
↑(s \ t) = ↑s \ ↑t
source
@[simp]
theorem topological_space.compact_opens.coe_compl {α : Type u_1} [topological_space α] [t2_space α] [compact_space α] (s : topological_space.compact_opens α) :
↑sᶜ = (↑s)ᶜ
source
@[protected, instance]
def topological_space.compact_opens.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.compact_opens α)
Equations
source
def topological_space.compact_opens.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
topological_space.compact_opens β

The image of a compact open under a continuous open map.

Equations
source
@[simp]
theorem topological_space.compact_opens.map_to_compacts {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
(topological_space.compact_opens.map f hf hf' s).to_compacts = topological_space.compacts.map f hf s.to_compacts
source
@[simp]
theorem topological_space.compact_opens.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
↑(topological_space.compact_opens.map f hf hf' s) = f '' ↑s