mathlib documentation

topology.sets.compacts

Compact sets #

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

Main Definitions #

For a topological space α,

Compact sets #

@[protected, ext]
theorem topological_space.compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.compacts α} (h : s = t) :
s = t
@[simp]
theorem topological_space.compacts.coe_mk {α : Type u_1} [topological_space α] (s : set α) (h : is_compact s) :
{carrier := s, compact' := h} = s
@[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]
@[simp]
theorem topological_space.compacts.coe_finset_sup {α : Type u_1} [topological_space α] {ι : Type u_2} {s : finset ι} {f : ι → topological_space.compacts α} :
(s.sup f) = s.sup (λ (i : ι), (f i))
@[protected]
def topological_space.compacts.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (K : topological_space.compacts α) :

The image of a compact set under a continuous function.

Equations
@[simp]
theorem topological_space.compacts.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (s : topological_space.compacts α) :
@[protected, 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.

@[protected]

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

Equations
@[simp]

Nonempty compact sets #

Reinterpret a nonempty compact as a closed set.

Equations
@[protected, ext]
@[protected, instance]
Equations
@[protected, instance]
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
@[protected]

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

Equations

Positive compact sets #

structure topological_space.positive_compacts (α : Type u_3) [topological_space α] :
Type u_3

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, ext]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem exists_positive_compacts_subset {α : Type u_1} [topological_space α] [locally_compact_space α] {U : set α} (ho : is_open U) (hn : U.nonempty) :
@[protected, instance]

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

@[protected]

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

Equations

Compact open sets #

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} [topological_space α] {s t : topological_space.compact_opens α} (h : s = t) :
s = t
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
  • topological_space.compact_opens.boolean_algebra = function.injective.boolean_algebra coe 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
def topological_space.compact_opens.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :

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

Equations
@[simp]
theorem topological_space.compact_opens.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
@[protected]

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

Equations