mathlib documentation

topology.compacts

Compact sets #

Summary #

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

Main Definitions #

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

The type of closed subsets of a topological space.

Equations
source
@[protected, instance]
def topological_space.closeds.inhabited (α : Type u_1) [topological_space α] :
inhabited (topological_space.closeds α)

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

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

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

Equations
source
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
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
@[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
source
def topological_space.positive_compacts_univ {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
topological_space.positive_compacts α

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

Equations
source
@[simp]
theorem topological_space.positive_compacts_univ_val (α : Type u_1) [topological_space α] [compact_space α] [nonempty α] :
topological_space.positive_compacts_univ.val = set.univ
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.order_bot {α : Type u_1} [topological_space α] :
order_bot (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.semilattice_inf {α : Type u_1} [topological_space α] [t2_space α] :
semilattice_inf (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.lattice {α : Type u_1} [topological_space α] [t2_space α] :
lattice (topological_space.compacts α)
Equations
source
@[simp]
theorem topological_space.compacts.bot_val {α : Type u_1} [topological_space α] :
⊥.val = ∅
source
@[simp]
theorem topological_space.compacts.sup_val {α : Type u_1} [topological_space α] {K₁ K₂ : topological_space.compacts α} :
(K₁ ⊔ K₂).val = K₁.val ∪ K₂.val
source
@[protected, ext]
theorem topological_space.compacts.ext {α : Type u_1} [topological_space α] {K₁ K₂ : topological_space.compacts α} (h : K₁.val = K₂.val) :
K₁ = K₂
source
@[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)
source
@[protected, instance]
def topological_space.compacts.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.compacts α)
Equations
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.map_val {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (K : topological_space.compacts α) :
(topological_space.compacts.map f hf K).val = f '' K.val
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).val = ⇑(f.symm) ⁻¹' K.val

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

source
@[protected, instance]
def topological_space.nonempty_compacts.to_compact_space {α : Type u_1} [topological_space α] {p : topological_space.nonempty_compacts α} :
compact_space ↥(p.val)
source
@[protected, instance]
def topological_space.nonempty_compacts.to_nonempty {α : Type u_1} [topological_space α] {p : topological_space.nonempty_compacts α} :
nonempty ↥(p.val)
source
def topological_space.nonempty_compacts.to_closeds {α : Type u_1} [topological_space α] [t2_space α] :
topological_space.nonempty_compacts α → topological_space.closeds α

Associate to a nonempty compact subset the corresponding closed subset

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

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