# mathlib3documentation

topology.sets.compacts

# Compact sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main Definitions #

For a topological space α,

• compacts α: The type of compact sets.
• nonempty_compacts α: The type of non-empty compact sets.
• positive_compacts α: The type of compact sets with non-empty interior.
• compact_opens α: The type of compact open sets. This is a central object in the study of spectral spaces.

### Compact sets #

structure topological_space.compacts (α : Type u_4)  :
Type u_4

The type of compact sets of a topological space.

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

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

Equations
@[simp]
@[simp]
@[simp]
theorem topological_space.compacts.coe_top {α : Type u_1}  :
@[simp]
theorem topological_space.compacts.coe_bot {α : Type u_1}  :
@[simp]
theorem topological_space.compacts.coe_finset_sup {α : Type u_1} {ι : Type u_2} {s : finset ι} {f : ι } :
(s.sup f) = s.sup (λ (i : ι), (f i))
@[protected]
def topological_space.compacts.map {α : Type u_1} {β : Type u_2} (f : α β) (hf : continuous f)  :

The image of a compact set under a continuous function.

Equations
@[simp, norm_cast]
theorem topological_space.compacts.coe_map {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f)  :
s) = f '' s
@[simp]
theorem topological_space.compacts.map_id {α : Type u_1}  :
theorem topological_space.compacts.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (g : α β) (hf : continuous f) (hg : continuous g)  :
_ K =
@[simp]
theorem topological_space.compacts.equiv_apply {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β)  :
@[protected]
def topological_space.compacts.equiv {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :

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

Equations
@[simp]
theorem topological_space.compacts.equiv_symm_apply {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β)  :
@[simp]
@[simp]
theorem topological_space.compacts.equiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ≃ₜ β) (g : β ≃ₜ γ) :
@[simp]
theorem topological_space.compacts.equiv_symm {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :
theorem topological_space.compacts.coe_equiv_apply_eq_preimage {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β)  :

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

@[protected]
def topological_space.compacts.prod {α : Type u_1} {β : Type u_2}  :

The product of two compacts, as a compacts in the product space.

Equations
@[simp]
theorem topological_space.compacts.coe_prod {α : Type u_1} {β : Type u_2}  :
(K.prod L) = K ×ˢ L

### Nonempty compact sets #

structure topological_space.nonempty_compacts (α : Type u_4)  :
Type u_4

The type of nonempty compact sets of a topological space.

Instances for topological_space.nonempty_compacts
@[protected, instance]
Equations
@[protected]
@[protected]

Reinterpret a nonempty compact as a closed set.

Equations
@[protected, ext]
theorem topological_space.nonempty_compacts.ext {α : Type u_1} (h : s = t) :
s = t
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected, instance]

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

Equations
@[protected, instance]
@[protected, instance]
@[protected]
def topological_space.nonempty_compacts.prod {α : Type u_1} {β : Type u_2}  :

The product of two nonempty_compacts, as a nonempty_compacts in the product space.

Equations
@[simp]
theorem topological_space.nonempty_compacts.coe_prod {α : Type u_1} {β : Type u_2}  :
(K.prod L) = K ×ˢ L

### Positive compact sets #

structure topological_space.positive_compacts (α : Type u_4)  :
Type u_4

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

Instances for topological_space.positive_compacts
@[protected, instance]
Equations
@[protected]
@[protected]

Reinterpret a positive compact as a nonempty compact.

Equations
@[protected, ext]
theorem topological_space.positive_compacts.ext {α : Type u_1} (h : s = t) :
s = t
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected]
def topological_space.positive_compacts.map {α : Type u_1} {β : Type u_2} (f : α β) (hf : continuous f) (hf' : is_open_map f)  :

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

Equations
@[simp, norm_cast]
theorem topological_space.positive_compacts.coe_map {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (hf' : is_open_map f)  :
s) = f '' s
@[simp]
theorem topological_space.positive_compacts.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (g : α β) (hf : continuous f) (hg : continuous g) (hf' : is_open_map f) (hg' : is_open_map g)  :
_ K = K)
theorem exists_positive_compacts_subset {α : Type u_1} {U : set α} (ho : is_open U) (hn : U.nonempty) :
(K : , K U
@[protected, instance]
Equations
@[protected, instance]

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

@[protected]
def topological_space.positive_compacts.prod {α : Type u_1} {β : Type u_2}  :

The product of two positive_compacts, as a positive_compacts in the product space.

Equations
@[simp]
theorem topological_space.positive_compacts.coe_prod {α : Type u_1} {β : Type u_2}  :
(K.prod L) = K ×ˢ L

### Compact open sets #

structure topological_space.compact_opens (α : Type u_4)  :
Type u_4
• to_compacts :
• is_open' :

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

Instances for topological_space.compact_opens
@[protected]
@[protected]

Reinterpret a compact open as an open.

Equations

Reinterpret a compact open as a clopen.

Equations
@[protected, ext]
theorem topological_space.compact_opens.ext {α : Type u_1} {s t : topological_space.compact_opens α} (h : s = t) :
s = t
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
• topological_space.compact_opens.generalized_boolean_algebra = topological_space.compact_opens.generalized_boolean_algebra._proof_1 topological_space.compact_opens.generalized_boolean_algebra._proof_2 topological_space.compact_opens.generalized_boolean_algebra._proof_3 topological_space.compact_opens.generalized_boolean_algebra._proof_4 topological_space.compact_opens.generalized_boolean_algebra._proof_5
@[protected, instance]
Equations
@[protected, instance]
Equations
• topological_space.compact_opens.boolean_algebra = 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
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
def topological_space.compact_opens.map {α : Type u_1} {β : Type u_2} (f : α β) (hf : continuous f) (hf' : is_open_map f)  :

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

Equations
@[simp]
theorem topological_space.compact_opens.map_to_compacts {α : Type u_1} {β : Type u_2} (f : α β) (hf : continuous f) (hf' : is_open_map f)  :
hf' s).to_compacts =
@[simp, norm_cast]
theorem topological_space.compact_opens.coe_map {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (hf' : is_open_map f)  :
hf' s) = f '' s
@[simp]
theorem topological_space.compact_opens.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (g : α β) (hf : continuous f) (hg : continuous g) (hf' : is_open_map f) (hg' : is_open_map g)  :
_ K = hg' K)
@[protected]
def topological_space.compact_opens.prod {α : Type u_1} {β : Type u_2}  :

The product of two compact_opens, as a compact_opens in the product space.

Equations
@[simp]
theorem topological_space.compact_opens.coe_prod {α : Type u_1} {β : Type u_2}  :
(K.prod L) = K ×ˢ L