Compact sets #

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

Main Definitions #

For a topological space α,

• TopologicalSpace.Compacts α: The type of compact sets.
• TopologicalSpace.NonemptyCompacts α: The type of non-empty compact sets.
• TopologicalSpace.PositiveCompacts α: The type of compact sets with non-empty interior.
• TopologicalSpace.CompactOpens α: The type of compact open sets. This is a central object in the study of spectral spaces.

Compact sets #

structure TopologicalSpace.Compacts (α : Type u_4) [] :
Type u_4

The type of compact sets of a topological space.

• carrier : Set α

the carrier set, i.e. the points in this set

• isCompact' : IsCompact self.carrier
Instances For
theorem TopologicalSpace.Compacts.isCompact' {α : Type u_4} [] (self : ) :
IsCompact self.carrier
Equations
• TopologicalSpace.Compacts.instSetLike = { coe := TopologicalSpace.Compacts.carrier, coe_injective' := }
def TopologicalSpace.Compacts.Simps.coe {α : Type u_1} [] (s : ) :
Set α

See Note [custom simps projection].

Equations
Instances For
theorem TopologicalSpace.Compacts.isCompact {α : Type u_1} [] (s : ) :
Equations
• =
instance TopologicalSpace.Compacts.instCanLiftSetCoeIsCompact {α : Type u_1} [] :
CanLift (Set α) SetLike.coe IsCompact
Equations
• =
theorem TopologicalSpace.Compacts.ext {α : Type u_1} [] {s : } {t : } (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.Compacts.coe_mk {α : Type u_1} [] (s : Set α) (h : ) :
{ carrier := s, isCompact' := h } = s
@[simp]
theorem TopologicalSpace.Compacts.carrier_eq_coe {α : Type u_1} [] (s : ) :
s.carrier = s
instance TopologicalSpace.Compacts.instSup {α : Type u_1} [] :
Equations
• TopologicalSpace.Compacts.instSup = { sup := fun (s t : ) => { carrier := s t, isCompact' := } }
Equations
• TopologicalSpace.Compacts.instInfOfT2Space = { inf := fun (s t : ) => { carrier := s t, isCompact' := } }
Equations
• TopologicalSpace.Compacts.instTopOfCompactSpace = { top := { carrier := Set.univ, isCompact' := } }
instance TopologicalSpace.Compacts.instBot {α : Type u_1} [] :
Equations
• TopologicalSpace.Compacts.instBot = { bot := { carrier := , isCompact' := } }
Equations
Equations
Equations
• TopologicalSpace.Compacts.instOrderBot = OrderBot.lift SetLike.coe
Equations
• TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace = BoundedOrder.lift SetLike.coe

The type of compact sets is inhabited, with default element the empty set.

Equations
• TopologicalSpace.Compacts.instInhabited = { default := }
@[simp]
theorem TopologicalSpace.Compacts.coe_sup {α : Type u_1} [] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem TopologicalSpace.Compacts.coe_inf {α : Type u_1} [] [] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem TopologicalSpace.Compacts.coe_top {α : Type u_1} [] [] :
= Set.univ
@[simp]
theorem TopologicalSpace.Compacts.coe_bot {α : Type u_1} [] :
=
@[simp]
theorem TopologicalSpace.Compacts.coe_finset_sup {α : Type u_1} [] {ι : Type u_4} {s : } {f : } :
(s.sup f) = s.sup fun (i : ι) => (f i)
def TopologicalSpace.Compacts.map {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) (K : ) :

The image of a compact set under a continuous function.

Equations
• = { carrier := f '' K.carrier, isCompact' := }
Instances For
@[simp]
theorem TopologicalSpace.Compacts.coe_map {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : ) :
() = f '' s
@[simp]
theorem TopologicalSpace.Compacts.map_id {α : Type u_1} [] (K : ) :
= K
theorem TopologicalSpace.Compacts.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : βγ) (g : αβ) (hf : ) (hg : ) (K : ) :
@[simp]
theorem TopologicalSpace.Compacts.equiv_symm_apply {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) (K : ) :
.symm K = TopologicalSpace.Compacts.map f.symm K
@[simp]
theorem TopologicalSpace.Compacts.equiv_apply {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) (K : ) :
def TopologicalSpace.Compacts.equiv {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :

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

Equations
Instances For
@[simp]
@[simp]
theorem TopologicalSpace.Compacts.equiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
@[simp]
theorem TopologicalSpace.Compacts.equiv_symm {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :
= .symm
theorem TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) (K : ) :
() = f.symm ⁻¹' K

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

def TopologicalSpace.Compacts.prod {α : Type u_1} {β : Type u_2} [] [] (K : ) (L : ) :

The product of two TopologicalSpace.Compacts, as a TopologicalSpace.Compacts in the product space.

Equations
• K.prod L = { carrier := K ×ˢ L, isCompact' := }
Instances For
@[simp]
theorem TopologicalSpace.Compacts.coe_prod {α : Type u_1} {β : Type u_2} [] [] (K : ) (L : ) :
(K.prod L) = K ×ˢ L

Nonempty compact sets #

structure TopologicalSpace.NonemptyCompacts (α : Type u_4) [] extends :
Type u_4

The type of nonempty compact sets of a topological space.

• carrier : Set α
• isCompact' : IsCompact self.carrier
• nonempty' : self.carrier.Nonempty
Instances For
theorem TopologicalSpace.NonemptyCompacts.nonempty' {α : Type u_4} [] (self : ) :
self.carrier.Nonempty
Equations
• TopologicalSpace.NonemptyCompacts.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }

See Note [custom simps projection].

Equations
Instances For
theorem TopologicalSpace.NonemptyCompacts.nonempty {α : Type u_1} [] :
(s).Nonempty

Reinterpret a nonempty compact as a closed set.

Equations
• s.toCloseds = { carrier := s, closed' := }
Instances For
theorem TopologicalSpace.NonemptyCompacts.ext {α : Type u_1} [] (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.NonemptyCompacts.coe_mk {α : Type u_1} [] (s : ) (h : s.carrier.Nonempty) :
{ toCompacts := s, nonempty' := h } = s
theorem TopologicalSpace.NonemptyCompacts.carrier_eq_coe {α : Type u_1} [] :
s.carrier = s
@[simp]
theorem TopologicalSpace.NonemptyCompacts.coe_toCompacts {α : Type u_1} [] :
s.toCompacts = s
Equations
• TopologicalSpace.NonemptyCompacts.instSup = { sup := fun (s t : ) => { toCompacts := s.toCompacts t.toCompacts, nonempty' := } }
Equations
• TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty = { top := { toCompacts := , nonempty' := } }
Equations
Equations
• TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty = OrderTop.lift SetLike.coe
@[simp]
theorem TopologicalSpace.NonemptyCompacts.coe_sup {α : Type u_1} [] :
(s t) = s t
@[simp]
theorem TopologicalSpace.NonemptyCompacts.coe_top {α : Type u_1} [] [] [] :
= Set.univ

In an inhabited space, the type of nonempty compact subsets is also inhabited, with default element the singleton set containing the default element.

Equations
• TopologicalSpace.NonemptyCompacts.instInhabited = { default := { carrier := {default}, isCompact' := , nonempty' := } }
Equations
• =
Equations
• =
def TopologicalSpace.NonemptyCompacts.prod {α : Type u_1} {β : Type u_2} [] [] :

The product of two TopologicalSpace.NonemptyCompacts, as a TopologicalSpace.NonemptyCompacts in the product space.

Equations
• K.prod L = let __src := K.prod L.toCompacts; { toCompacts := __src, nonempty' := }
Instances For
@[simp]
theorem TopologicalSpace.NonemptyCompacts.coe_prod {α : Type u_1} {β : Type u_2} [] [] :
(K.prod L) = K ×ˢ L

Positive compact sets #

structure TopologicalSpace.PositiveCompacts (α : Type u_4) [] extends :
Type u_4

The type of compact sets with nonempty interior of a topological space. See also TopologicalSpace.Compacts and TopologicalSpace.NonemptyCompacts.

• carrier : Set α
• isCompact' : IsCompact self.carrier
• interior_nonempty' : (interior self.carrier).Nonempty
Instances For
theorem TopologicalSpace.PositiveCompacts.interior_nonempty' {α : Type u_4} [] (self : ) :
(interior self.carrier).Nonempty
Equations
• TopologicalSpace.PositiveCompacts.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }

See Note [custom simps projection].

Equations
Instances For
theorem TopologicalSpace.PositiveCompacts.nonempty {α : Type u_1} [] :
(s).Nonempty

Reinterpret a positive compact as a nonempty compact.

Equations
• s.toNonemptyCompacts = { toCompacts := s.toCompacts, nonempty' := }
Instances For
theorem TopologicalSpace.PositiveCompacts.ext {α : Type u_1} [] (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.PositiveCompacts.coe_mk {α : Type u_1} [] (s : ) (h : (interior s.carrier).Nonempty) :
{ toCompacts := s, interior_nonempty' := h } = s
theorem TopologicalSpace.PositiveCompacts.carrier_eq_coe {α : Type u_1} [] :
s.carrier = s
@[simp]
theorem TopologicalSpace.PositiveCompacts.coe_toCompacts {α : Type u_1} [] :
s.toCompacts = s
Equations
• TopologicalSpace.PositiveCompacts.instSup = { sup := fun (s t : ) => { toCompacts := s.toCompacts t.toCompacts, interior_nonempty' := } }
Equations
• TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty = { top := { toCompacts := , interior_nonempty' := } }
Equations
Equations
• TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty = OrderTop.lift SetLike.coe
@[simp]
theorem TopologicalSpace.PositiveCompacts.coe_sup {α : Type u_1} [] :
(s t) = s t
@[simp]
theorem TopologicalSpace.PositiveCompacts.coe_top {α : Type u_1} [] [] [] :
= Set.univ
def TopologicalSpace.PositiveCompacts.map {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) (hf' : ) :

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

Equations
Instances For
@[simp]
theorem TopologicalSpace.PositiveCompacts.coe_map {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (hf' : ) :
() = f '' s
@[simp]
theorem TopologicalSpace.PositiveCompacts.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : βγ) (g : αβ) (hf : ) (hg : ) (hf' : ) (hg' : ) :
theorem exists_positiveCompacts_subset {α : Type u_1} [] {U : Set α} (ho : ) (hn : U.Nonempty) :
∃ (K : ), K U
theorem IsOpen.exists_positiveCompacts_closure_subset {α : Type u_1} [] [] {U : Set α} (ho : ) (hn : U.Nonempty) :
∃ (K : ), closure K U
Equations
• TopologicalSpace.PositiveCompacts.instInhabitedOfCompactSpaceOfNonempty = { default := }

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

Equations
• =
def TopologicalSpace.PositiveCompacts.prod {α : Type u_1} {β : Type u_2} [] [] :

The product of two TopologicalSpace.PositiveCompacts, as a TopologicalSpace.PositiveCompacts in the product space.

Equations
• K.prod L = { toCompacts := K.prod L.toCompacts, interior_nonempty' := }
Instances For
@[simp]
theorem TopologicalSpace.PositiveCompacts.coe_prod {α : Type u_1} {β : Type u_2} [] [] :
(K.prod L) = K ×ˢ L

Compact open sets #

structure TopologicalSpace.CompactOpens (α : Type u_4) [] extends :
Type u_4

The type of compact open sets of a topological space. This is useful in non Hausdorff contexts, in particular spectral spaces.

Instances For
theorem TopologicalSpace.CompactOpens.isOpen' {α : Type u_4} [] (self : ) :
IsOpen self.carrier
Equations
• TopologicalSpace.CompactOpens.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }

See Note [custom simps projection].

Equations
Instances For
@[simp]
theorem TopologicalSpace.CompactOpens.toOpens_coe {α : Type u_1} [] :
s.toOpens = s

Reinterpret a compact open as an open.

Equations
• s.toOpens = { carrier := s, is_open' := }
Instances For
@[simp]
theorem TopologicalSpace.CompactOpens.toClopens_coe {α : Type u_1} [] [] :
s.toClopens = s

Reinterpret a compact open as a clopen.

Equations
• s.toClopens = { carrier := s, isClopen' := }
Instances For
theorem TopologicalSpace.CompactOpens.ext {α : Type u_1} [] (h : s = t) :
s = t
@[simp]
theorem TopologicalSpace.CompactOpens.coe_mk {α : Type u_1} [] (s : ) (h : IsOpen s.carrier) :
{ toCompacts := s, isOpen' := h } = s
Equations
• TopologicalSpace.CompactOpens.instSup = { sup := fun (s t : ) => { toCompacts := s.toCompacts t.toCompacts, isOpen' := } }
Equations
• TopologicalSpace.CompactOpens.instBot = { bot := { toCompacts := , isOpen' := } }
@[simp]
theorem TopologicalSpace.CompactOpens.coe_sup {α : Type u_1} [] :
(s t) = s t
@[simp]
Equations
Equations
• TopologicalSpace.CompactOpens.instOrderBot = OrderBot.lift SetLike.coe
Equations
• TopologicalSpace.CompactOpens.instInhabited = { default := }
Equations
• TopologicalSpace.CompactOpens.instInf = { inf := fun (U V : ) => { carrier := U V, isCompact' := , isOpen' := } }
@[simp]
theorem TopologicalSpace.CompactOpens.coe_inf {α : Type u_1} [] :
(s t) = s t
Equations
instance TopologicalSpace.CompactOpens.instSDiff {α : Type u_1} [] [] :
Equations
• TopologicalSpace.CompactOpens.instSDiff = { sdiff := fun (s t : ) => { carrier := s \ t, isCompact' := , isOpen' := } }
@[simp]
theorem TopologicalSpace.CompactOpens.coe_sdiff {α : Type u_1} [] [] :
(s \ t) = s \ t
Equations
instance TopologicalSpace.CompactOpens.instTop {α : Type u_1} [] [] :
Equations
• TopologicalSpace.CompactOpens.instTop = { top := { toCompacts := , isOpen' := } }
@[simp]
theorem TopologicalSpace.CompactOpens.coe_top {α : Type u_1} [] [] :
= Set.univ
Equations
• TopologicalSpace.CompactOpens.instBoundedOrder = BoundedOrder.lift SetLike.coe
instance TopologicalSpace.CompactOpens.instHasCompl {α : Type u_1} [] [] [] :
Equations
• TopologicalSpace.CompactOpens.instHasCompl = { compl := fun (s : ) => { carrier := (s), isCompact' := , isOpen' := } }
instance TopologicalSpace.CompactOpens.instHImp {α : Type u_1} [] [] [] :
Equations
• TopologicalSpace.CompactOpens.instHImp = { himp := fun (s t : ) => { carrier := s t, isCompact' := , isOpen' := } }
@[simp]
theorem TopologicalSpace.CompactOpens.coe_compl {α : Type u_1} [] [] [] :
s = (s)
@[simp]
theorem TopologicalSpace.CompactOpens.coe_himp {α : Type u_1} [] [] [] :
(s t) = s t
Equations
@[simp]
theorem TopologicalSpace.CompactOpens.map_toCompacts {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) (hf' : ) :
().toCompacts = TopologicalSpace.Compacts.map f hf s.toCompacts
def TopologicalSpace.CompactOpens.map {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) (hf' : ) :

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

Equations
Instances For
@[simp]
theorem TopologicalSpace.CompactOpens.coe_map {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (hf' : ) :
() = f '' s
@[simp]
theorem TopologicalSpace.CompactOpens.map_id {α : Type u_1} [] :
= K
theorem TopologicalSpace.CompactOpens.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : βγ) (g : αβ) (hf : ) (hg : ) (hf' : ) (hg' : ) :
def TopologicalSpace.CompactOpens.prod {α : Type u_1} {β : Type u_2} [] [] :

The product of two TopologicalSpace.CompactOpens, as a TopologicalSpace.CompactOpens in the product space.

Equations
• K.prod L = let __src := K.prod L.toCompacts; { toCompacts := __src, isOpen' := }
Instances For
@[simp]
theorem TopologicalSpace.CompactOpens.coe_prod {α : Type u_1} {β : Type u_2} [] [] :
(K.prod L) = K ×ˢ L