mathlib documentation

topology.compacts

Compact sets

Summary

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

Main Definitions

def topological_space.closeds (α : Type u_1) [topological_space α] :
Type u_1

The type of closed subsets of a topological space.

Equations
@[instance]

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

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

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

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

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

Equations
@[instance]

Equations
@[simp]

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

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

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

def topological_space.compacts.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (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} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (K : topological_space.compacts α) :

@[simp]

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

Equations

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

Associate to a nonempty compact subset the corresponding closed subset

Equations