# mathlibdocumentation

topology.compacts

# Compact sets

## Summary

We define the subtype of compact sets in a topological space.

## Main Definitions

• closeds α is the type of closed subsets of a topological space α.
• compacts α is the type of compact subsets of a topological space α.
• nonempty_compacts α is the type of non-empty compact subsets.
• positive_compacts α is the type of compact subsets with non-empty interior.
def topological_space.closeds (α : Type u_1)  :
Type u_1

The type of closed subsets of a topological space.

Equations
• = {s //
@[instance]
def topological_space.inhabited (α : Type u_1)  :

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

Equations
def topological_space.compacts (α : Type u_1)  :
Type u_1

The compact sets of a topological space. See also nonempty_compacts.

Equations
• = {s //
def topological_space.nonempty_compacts (α : Type u_1)  :
Type u_1

The type of non-empty compact subsets of a topological space. The non-emptiness will be useful in metric spaces, as we will be able to put a distance (and not merely an edistance) on this space.

Equations
@[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
@[nolint]
def topological_space.positive_compacts (α : Type u_1)  :
Type u_1

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

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def topological_space.compacts.lattice {α : Type u_1} [t2_space α] :

Equations
@[simp]
theorem topological_space.compacts.bot_val {α : Type u_1}  :

@[simp]
theorem topological_space.compacts.sup_val {α : Type u_1} {K₁ K₂ : topological_space.compacts α} :
(K₁ K₂).val = K₁.val K₂.val

@[ext]
theorem topological_space.compacts.ext {α : Type u_1} {K₁ K₂ : topological_space.compacts α} :
K₁.val = K₂.valK₁ = K₂

@[simp]
theorem topological_space.compacts.finset_sup_val {α : Type u_1} {β : Type u_2} {K : β → } {s : finset β} :
(s.sup K).val = s.sup (λ (x : β), (K x).val)

@[instance]
def topological_space.compacts.inhabited {α : Type u_1}  :

Equations
def topological_space.compacts.map {α : Type u_1} {β : Type u_2} (f : α → β) :

The image of a compact set under a continuous function.

Equations
@[simp]
theorem topological_space.compacts.map_val {α : Type u_1} {β : Type u_2} {f : α → β} (hf : continuous f)  :
K).val = f '' K.val

@[simp]
def topological_space.compacts.equiv {α : Type u_1} {β : Type u_2}  :

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

Equations
theorem topological_space.compacts.equiv_to_fun_val {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β)  :

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

@[instance]

@[instance]

Associate to a nonempty compact subset the corresponding closed subset

Equations