mathlib3 documentation

topology.sets.compacts

Compact sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, is_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]
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]

The image of a compact set under a continuous function.

Equations
@[simp, norm_cast]
@[protected]

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

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 #

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
@[protected]

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

Equations
@[simp, norm_cast]
@[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]
@[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

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

Equations
@[simp, norm_cast]
@[protected]

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

Equations