# 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 //
@[protected, instance]
def topological_space.closeds.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
@[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
@[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

In a nonempty compact space, set.univ is a member of positive_compacts, the compact sets with nonempty interior.

Equations
@[simp]
theorem topological_space.positive_compacts_univ_val (α : Type u_1) [nonempty α] :
@[protected, instance]
Equations
@[protected, instance]
def topological_space.compacts.order_bot {α : Type u_1}  :
Equations
@[protected, instance]
Equations
@[protected, 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
@[protected, ext]
theorem topological_space.compacts.ext {α : Type u_1} {K₁ K₂ : topological_space.compacts α} (h : K₁.val = K₂.val) :
K₁ = 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)
@[protected, instance]
def topological_space.compacts.inhabited {α : Type u_1}  :
Equations
@[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]
theorem topological_space.compacts.map_val {α : Type u_1} {β : Type u_2} {f : α → β} (hf : continuous f)  :
K).val = f '' K.val
@[protected, simp]
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
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.

@[protected, instance]
@[protected, instance]

Associate to a nonempty compact subset the corresponding closed subset

Equations
@[protected, instance]
def topological_space.nonempty_positive_compacts (α : Type u_1) [h : nonempty α] :

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