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.
The type of closed subsets of a topological space.
Equations
- topological_space.closeds α = {s // is_closed s}
The compact sets of a topological space. See also nonempty_compacts.
Equations
- topological_space.compacts α = {s // is_compact s}
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
- topological_space.nonempty_compacts α = {s // s.nonempty ∧ is_compact s}
@[nolint]
The compact sets with nonempty interior of a topological space. See also compacts and
nonempty_compacts.
Equations
- topological_space.positive_compacts α = {s // is_compact s ∧ (interior s).nonempty}
@[instance]
Equations
- topological_space.compacts.semilattice_sup_bot = subtype.semilattice_sup_bot compact_empty topological_space.compacts.semilattice_sup_bot._proof_1
@[instance]
def
topological_space.compacts.semilattice_inf_bot
{α : Type u_1}
[topological_space α]
[t2_space α] :
Equations
- topological_space.compacts.semilattice_inf_bot = subtype.semilattice_inf_bot compact_empty topological_space.compacts.semilattice_inf_bot._proof_1
@[instance]
Equations
- topological_space.compacts.lattice = subtype.lattice topological_space.compacts.lattice._proof_1 topological_space.compacts.lattice._proof_2
@[simp]
@[simp]
theorem
topological_space.compacts.sup_val
{α : Type u_1}
[topological_space α]
{K₁ K₂ : topological_space.compacts α} :
@[ext]
theorem
topological_space.compacts.ext
{α : Type u_1}
[topological_space α]
{K₁ K₂ : topological_space.compacts α} :
@[simp]
theorem
topological_space.compacts.finset_sup_val
{α : Type u_1}
[topological_space α]
{β : Type u_2}
{K : β → topological_space.compacts α}
{s : finset β} :
@[instance]
Equations
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
- topological_space.compacts.map f hf K = ⟨f '' K.val, _⟩
@[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
@[simp]
def
topological_space.compacts.equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
A homeomorphism induces an equivalence on compact sets, by taking the image.
Equations
- topological_space.compacts.equiv f = {to_fun := topological_space.compacts.map ⇑f _, inv_fun := topological_space.compacts.map ⇑(f.symm) _, left_inv := _, right_inv := _}
theorem
topological_space.compacts.equiv_to_fun_val
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ₜ β)
(K : topological_space.compacts α) :
The image of a compact set under a homeomorphism can also be expressed as a preimage.
@[instance]
def
topological_space.nonempty_compacts.to_compact_space
{α : Type u_1}
[topological_space α]
{p : topological_space.nonempty_compacts α} :
compact_space ↥(p.val)
@[instance]
def
topological_space.nonempty_compacts.to_nonempty
{α : Type u_1}
[topological_space α]
{p : topological_space.nonempty_compacts α} :
Equations
def
topological_space.nonempty_compacts.to_closeds
{α : Type u_1}
[topological_space α]
[t2_space α] :
Associate to a nonempty compact subset the corresponding closed subset
Equations
- topological_space.nonempty_compacts.to_closeds = set.inclusion topological_space.nonempty_compacts.to_closeds._proof_1