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 #
The type of compact sets of a topological space.
- carrier : Set α
the carrier set, i.e. the points in this set
Instances For
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instPartialOrder
{α : Type u_1}
[TopologicalSpace α]
:
PartialOrder (Compacts α)
See Note [custom simps projection].
Instances For
theorem
TopologicalSpace.Compacts.isCompact
{α : Type u_1}
[TopologicalSpace α]
(s : Compacts α)
:
IsCompact ↑s
instance
TopologicalSpace.Compacts.instCompactSpaceSubtypeMem
{α : Type u_1}
[TopologicalSpace α]
(K : Compacts α)
:
CompactSpace ↥K
def
TopologicalSpace.Compacts.toCloseds
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : Compacts α)
:
Closeds α
Reinterpret a compact as a closed set.
Instances For
@[simp]
theorem
TopologicalSpace.Compacts.coe_toCloseds
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : Compacts α)
:
↑s.toCloseds = ↑s
@[simp]
theorem
TopologicalSpace.Compacts.mem_toCloseds
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
{x : α}
{s : Compacts α}
:
x ∈ s.toCloseds ↔ x ∈ s
theorem
TopologicalSpace.Compacts.toCloseds_injective
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
:
Function.Injective toCloseds
instance
TopologicalSpace.Compacts.instCanLiftSetCoeIsCompact
{α : Type u_1}
[TopologicalSpace α]
:
CanLift (Set α) (Compacts α) SetLike.coe IsCompact
theorem
TopologicalSpace.Compacts.ext
{α : Type u_1}
[TopologicalSpace α]
{s t : Compacts α}
(h : ↑s = ↑t)
:
s = t
theorem
TopologicalSpace.Compacts.ext_iff
{α : Type u_1}
[TopologicalSpace α]
{s t : Compacts α}
:
s = t ↔ ↑s = ↑t
@[simp]
theorem
TopologicalSpace.Compacts.coe_mk
{α : Type u_1}
[TopologicalSpace α]
(s : Set α)
(h : IsCompact s)
:
@[simp]
theorem
TopologicalSpace.Compacts.carrier_eq_coe
{α : Type u_1}
[TopologicalSpace α]
(s : Compacts α)
:
s.carrier = ↑s
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instMinOfT2Space
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
:
Min (Compacts α)
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instTopOfCompactSpace
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
:
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instDistribLatticeOfT2Space
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
:
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
:
BoundedOrder (Compacts α)
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instInhabited
{α : Type u_1}
[TopologicalSpace α]
:
Inhabited (Compacts α)
The type of compact sets is inhabited, with default element the empty set.
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instUniqueOfIsEmpty
{α : Type u_1}
[TopologicalSpace α]
[IsEmpty α]
:
@[simp]
theorem
TopologicalSpace.Compacts.coe_sup
{α : Type u_1}
[TopologicalSpace α]
(s t : Compacts α)
:
↑(s ⊔ t) = ↑s ∪ ↑t
@[simp]
theorem
TopologicalSpace.Compacts.coe_inf
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s t : Compacts α)
:
↑(s ⊓ t) = ↑s ∩ ↑t
@[simp]
@[simp]
@[simp]
theorem
TopologicalSpace.Compacts.coe_eq_empty
{α : Type u_1}
[TopologicalSpace α]
{s : Compacts α}
:
↑s = ∅ ↔ s = ⊥
@[simp]
theorem
TopologicalSpace.Compacts.coe_nonempty
{α : Type u_1}
[TopologicalSpace α]
{s : Compacts α}
:
@[simp]
theorem
TopologicalSpace.Compacts.coe_finset_sup
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_4}
{s : Finset ι}
{f : ι → Compacts α}
:
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instSingleton
{α : Type u_1}
[TopologicalSpace α]
:
Singleton α (Compacts α)
@[simp]
theorem
TopologicalSpace.Compacts.coe_singleton
{α : Type u_1}
[TopologicalSpace α]
(x : α)
:
↑{x} = {x}
@[simp]
theorem
TopologicalSpace.Compacts.mem_singleton
{α : Type u_1}
[TopologicalSpace α]
(x y : α)
:
x ∈ {y} ↔ x = y
@[simp]
theorem
TopologicalSpace.Compacts.toCloseds_singleton
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(x : α)
:
{x}.toCloseds = {x}
theorem
TopologicalSpace.Compacts.singleton_injective
{α : Type u_1}
[TopologicalSpace α]
:
Function.Injective fun (x : α) => {x}
@[simp]
theorem
TopologicalSpace.Compacts.singleton_inj
{α : Type u_1}
[TopologicalSpace α]
{x y : α}
:
{x} = {y} ↔ x = y
instance
TopologicalSpace.Compacts.instNontrivialOfNonempty
{α : Type u_1}
[TopologicalSpace α]
[Nonempty α]
:
Nontrivial (Compacts α)
@[simp]
@[simp]
theorem
TopologicalSpace.Compacts.nontrivial_iff
{α : Type u_1}
[TopologicalSpace α]
:
Nontrivial (Compacts α) ↔ Nonempty α
def
TopologicalSpace.Compacts.map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(K : Compacts α)
:
Compacts β
The image of a compact set under a continuous function.
Instances For
@[simp]
theorem
TopologicalSpace.Compacts.coe_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(s : Compacts α)
:
↑(Compacts.map f hf s) = f '' ↑s
@[simp]
theorem
TopologicalSpace.Compacts.map_id
{α : Type u_1}
[TopologicalSpace α]
(K : Compacts α)
:
Compacts.map id ⋯ K = K
theorem
TopologicalSpace.Compacts.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
(f : β → γ)
(g : α → β)
(hf : Continuous f)
(hg : Continuous g)
(K : Compacts α)
:
Compacts.map (f ∘ g) ⋯ K = Compacts.map f hf (Compacts.map g hg K)
theorem
TopologicalSpace.Compacts.map_injective
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(hf' : Function.Injective f)
:
Function.Injective (Compacts.map f hf)
@[simp]
theorem
TopologicalSpace.Compacts.map_singleton
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(x : α)
:
Compacts.map f hf {x} = {f x}
@[simp]
theorem
TopologicalSpace.Compacts.map_injective_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
:
Function.Injective (Compacts.map f hf) ↔ Function.Injective f
theorem
TopologicalSpace.Compacts.range_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Topology.IsInducing f)
:
def
TopologicalSpace.Compacts.equiv
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α ≃ₜ β)
:
A homeomorphism induces an equivalence on compact sets, by taking the image.
Instances For
@[simp]
theorem
TopologicalSpace.Compacts.equiv_apply
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α ≃ₜ β)
(K : Compacts α)
:
(Compacts.equiv f) K = Compacts.map ⇑f ⋯ K
@[simp]
theorem
TopologicalSpace.Compacts.equiv_symm_apply
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α ≃ₜ β)
(K : Compacts β)
:
(Compacts.equiv f).symm K = Compacts.map ⇑f.symm ⋯ K
@[simp]
theorem
TopologicalSpace.Compacts.equiv_refl
{α : Type u_1}
[TopologicalSpace α]
:
Compacts.equiv (Homeomorph.refl α) = Equiv.refl (Compacts α)
@[simp]
theorem
TopologicalSpace.Compacts.equiv_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
(f : α ≃ₜ β)
(g : β ≃ₜ γ)
:
Compacts.equiv (f.trans g) = (Compacts.equiv f).trans (Compacts.equiv g)
@[simp]
theorem
TopologicalSpace.Compacts.equiv_symm
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α ≃ₜ β)
:
Compacts.equiv f.symm = (Compacts.equiv f).symm
theorem
TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α ≃ₜ β)
(K : Compacts α)
:
↑((Compacts.equiv f) K) = ⇑f.symm ⁻¹' ↑K
The image of a compact set under a homeomorphism can also be expressed as a preimage.
@[implicit_reducible]
instance
TopologicalSpace.Compacts.instSProdProd
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
:
The product of two TopologicalSpace.Compacts, as a TopologicalSpace.Compacts in the product
space.
@[reducible, inline, deprecated "Use `K ×ˢ L` instead" (since := "2025-11-15")]
abbrev
TopologicalSpace.Compacts.prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : Compacts α)
(L : Compacts β)
:
Compacts (α × β)
The product of two TopologicalSpace.Compacts, as a TopologicalSpace.Compacts in the product
space.
Instances For
@[simp]
theorem
TopologicalSpace.Compacts.coe_prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : Compacts α)
(L : Compacts β)
:
@[simp]
theorem
TopologicalSpace.Compacts.toCloseds_prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[T2Space α]
[T2Space β]
(K : Compacts α)
(L : Compacts β)
:
@[simp]
theorem
TopologicalSpace.Compacts.singleton_prod_singleton
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α)
(y : β)
:
{x} ×ˢ {y} = {(x, y)}
Nonempty compact sets #
structure
TopologicalSpace.NonemptyCompacts
(α : Type u_4)
[TopologicalSpace α]
extends TopologicalSpace.Compacts α :
Type u_4
The type of nonempty compact sets of a topological space.
- isCompact' : IsCompact self.carrier
Instances For
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instSetLike
{α : Type u_1}
[TopologicalSpace α]
:
SetLike (NonemptyCompacts α) α
@[implicit_reducible]
def
TopologicalSpace.NonemptyCompacts.Simps.coe
{α : Type u_1}
[TopologicalSpace α]
(s : NonemptyCompacts α)
:
Set α
See Note [custom simps projection].
Instances For
theorem
TopologicalSpace.NonemptyCompacts.isCompact
{α : Type u_1}
[TopologicalSpace α]
(s : NonemptyCompacts α)
:
IsCompact ↑s
theorem
TopologicalSpace.NonemptyCompacts.nonempty
{α : Type u_1}
[TopologicalSpace α]
(s : NonemptyCompacts α)
:
(↑s).Nonempty
def
TopologicalSpace.NonemptyCompacts.toCloseds
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : NonemptyCompacts α)
:
Closeds α
Reinterpret a nonempty compact as a closed set.
Instances For
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_toCloseds
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : NonemptyCompacts α)
:
↑s.toCloseds = ↑s
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.toCloseds_toCompacts
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : NonemptyCompacts α)
:
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.mem_toCloseds
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
{x : α}
{s : NonemptyCompacts α}
:
x ∈ s.toCloseds ↔ x ∈ s
theorem
TopologicalSpace.NonemptyCompacts.toCloseds_injective
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
:
Function.Injective toCloseds
theorem
TopologicalSpace.NonemptyCompacts.ext
{α : Type u_1}
[TopologicalSpace α]
{s t : NonemptyCompacts α}
(h : ↑s = ↑t)
:
s = t
theorem
TopologicalSpace.NonemptyCompacts.ext_iff
{α : Type u_1}
[TopologicalSpace α]
{s t : NonemptyCompacts α}
:
s = t ↔ ↑s = ↑t
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_mk
{α : Type u_1}
[TopologicalSpace α]
(s : Compacts α)
(h : s.carrier.Nonempty)
:
theorem
TopologicalSpace.NonemptyCompacts.carrier_eq_coe
{α : Type u_1}
[TopologicalSpace α]
(s : NonemptyCompacts α)
:
s.carrier = ↑s
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_toCompacts
{α : Type u_1}
[TopologicalSpace α]
(s : NonemptyCompacts α)
:
↑s.toCompacts = ↑s
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.mem_toCompacts
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : NonemptyCompacts α}
:
x ∈ s.toCompacts ↔ x ∈ s
theorem
TopologicalSpace.NonemptyCompacts.toCompacts_injective
{α : Type u_1}
[TopologicalSpace α]
:
Function.Injective toCompacts
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.range_toCompacts
{α : Type u_1}
[TopologicalSpace α]
:
Set.range toCompacts = {⊥}ᶜ
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instMax
{α : Type u_1}
[TopologicalSpace α]
:
Max (NonemptyCompacts α)
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
Top (NonemptyCompacts α)
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_sup
{α : Type u_1}
[TopologicalSpace α]
(s t : NonemptyCompacts α)
:
↑(s ⊔ t) = ↑s ∪ ↑t
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_top
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instSingleton
{α : Type u_1}
[TopologicalSpace α]
:
Singleton α (NonemptyCompacts α)
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.toCompacts_singleton
{α : Type u_1}
[TopologicalSpace α]
(x : α)
:
{x}.toCompacts = {x}
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_singleton
{α : Type u_1}
[TopologicalSpace α]
(x : α)
:
↑{x} = {x}
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.mem_singleton
{α : Type u_1}
[TopologicalSpace α]
(x y : α)
:
x ∈ {y} ↔ x = y
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.toCloseds_singleton
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(x : α)
:
{x}.toCloseds = {x}
theorem
TopologicalSpace.NonemptyCompacts.singleton_injective
{α : Type u_1}
[TopologicalSpace α]
:
Function.Injective fun (x : α) => {x}
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.singleton_inj
{α : Type u_1}
[TopologicalSpace α]
{x y : α}
:
{x} = {y} ↔ x = y
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instInhabited
{α : Type u_1}
[TopologicalSpace α]
[Inhabited α]
:
Inhabited (NonemptyCompacts α)
In an inhabited space, the type of nonempty compact subsets is also inhabited, with default element the singleton set containing the default element.
instance
TopologicalSpace.NonemptyCompacts.instIsEmpty
{α : Type u_1}
[TopologicalSpace α]
[IsEmpty α]
:
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.isEmpty_iff
{α : Type u_1}
[TopologicalSpace α]
:
IsEmpty (NonemptyCompacts α) ↔ IsEmpty α
instance
TopologicalSpace.NonemptyCompacts.instNonempty
{α : Type u_1}
[TopologicalSpace α]
[Nonempty α]
:
Nonempty (NonemptyCompacts α)
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.nonempty_iff
{α : Type u_1}
[TopologicalSpace α]
:
Nonempty (NonemptyCompacts α) ↔ Nonempty α
instance
TopologicalSpace.NonemptyCompacts.instSubsingleton
{α : Type u_1}
[TopologicalSpace α]
[Subsingleton α]
:
Subsingleton (NonemptyCompacts α)
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.subsingleton_iff
{α : Type u_1}
[TopologicalSpace α]
:
Subsingleton (NonemptyCompacts α) ↔ Subsingleton α
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instUnique
{α : Type u_1}
[TopologicalSpace α]
[Unique α]
:
instance
TopologicalSpace.NonemptyCompacts.instNontrivial
{α : Type u_1}
[TopologicalSpace α]
[Nontrivial α]
:
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.nontrivial_iff
{α : Type u_1}
[TopologicalSpace α]
:
Nontrivial (NonemptyCompacts α) ↔ Nontrivial α
def
TopologicalSpace.NonemptyCompacts.map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(K : NonemptyCompacts α)
:
The image of a nonempty compact set under a continuous function.
Instances For
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.toCompacts_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(K : NonemptyCompacts α)
:
(NonemptyCompacts.map f hf K).toCompacts = Compacts.map f hf K.toCompacts
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(s : NonemptyCompacts α)
:
↑(NonemptyCompacts.map f hf s) = f '' ↑s
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.map_id
{α : Type u_1}
[TopologicalSpace α]
(K : NonemptyCompacts α)
:
NonemptyCompacts.map id ⋯ K = K
theorem
TopologicalSpace.NonemptyCompacts.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
(f : β → γ)
(g : α → β)
(hf : Continuous f)
(hg : Continuous g)
(K : NonemptyCompacts α)
:
NonemptyCompacts.map (f ∘ g) ⋯ K = NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.map_singleton
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(x : α)
:
NonemptyCompacts.map f hf {x} = {f x}
theorem
TopologicalSpace.NonemptyCompacts.map_injective
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(hf' : Function.Injective f)
:
Function.Injective (NonemptyCompacts.map f hf)
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.map_injective_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
:
Function.Injective (NonemptyCompacts.map f hf) ↔ Function.Injective f
theorem
TopologicalSpace.NonemptyCompacts.range_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Topology.IsInducing f)
:
Set.range (NonemptyCompacts.map f ⋯) = {K : NonemptyCompacts β | ↑K ⊆ Set.range f}
instance
TopologicalSpace.NonemptyCompacts.toCompactSpace
{α : Type u_1}
[TopologicalSpace α]
{s : NonemptyCompacts α}
:
CompactSpace ↥s
instance
TopologicalSpace.NonemptyCompacts.toNonempty
{α : Type u_1}
[TopologicalSpace α]
{s : NonemptyCompacts α}
:
Nonempty ↥s
@[implicit_reducible]
instance
TopologicalSpace.NonemptyCompacts.instSProdProd
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
:
SProd (NonemptyCompacts α) (NonemptyCompacts β) (NonemptyCompacts (α × β))
The product of two TopologicalSpace.NonemptyCompacts, as a TopologicalSpace.NonemptyCompacts
in the product space.
@[reducible, inline, deprecated "Use `K ×ˢ L` instead" (since := "2025-11-15")]
abbrev
TopologicalSpace.NonemptyCompacts.prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : NonemptyCompacts α)
(L : NonemptyCompacts β)
:
NonemptyCompacts (α × β)
The product of two TopologicalSpace.NonemptyCompacts, as a TopologicalSpace.NonemptyCompacts
in the product space.
Instances For
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.coe_prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : NonemptyCompacts α)
(L : NonemptyCompacts β)
:
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.toCloseds_prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[T2Space α]
[T2Space β]
(K : NonemptyCompacts α)
(L : NonemptyCompacts β)
:
@[simp]
theorem
TopologicalSpace.NonemptyCompacts.singleton_prod_singleton
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α)
(y : β)
:
{x} ×ˢ {y} = {(x, y)}
Positive compact sets #
structure
TopologicalSpace.PositiveCompacts
(α : Type u_4)
[TopologicalSpace α]
extends TopologicalSpace.Compacts α :
Type u_4
The type of compact sets with nonempty interior of a topological space.
See also TopologicalSpace.Compacts and TopologicalSpace.NonemptyCompacts.
- isCompact' : IsCompact self.carrier
Instances For
@[implicit_reducible]
instance
TopologicalSpace.PositiveCompacts.instSetLike
{α : Type u_1}
[TopologicalSpace α]
:
SetLike (PositiveCompacts α) α
@[implicit_reducible]
def
TopologicalSpace.PositiveCompacts.Simps.coe
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
Set α
See Note [custom simps projection].
Instances For
theorem
TopologicalSpace.PositiveCompacts.isCompact
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
IsCompact ↑s
theorem
TopologicalSpace.PositiveCompacts.interior_nonempty
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
theorem
TopologicalSpace.PositiveCompacts.nonempty
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
(↑s).Nonempty
def
TopologicalSpace.PositiveCompacts.toNonemptyCompacts
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
Reinterpret a positive compact as a nonempty compact.
Instances For
theorem
TopologicalSpace.PositiveCompacts.ext
{α : Type u_1}
[TopologicalSpace α]
{s t : PositiveCompacts α}
(h : ↑s = ↑t)
:
s = t
theorem
TopologicalSpace.PositiveCompacts.ext_iff
{α : Type u_1}
[TopologicalSpace α]
{s t : PositiveCompacts α}
:
s = t ↔ ↑s = ↑t
@[simp]
theorem
TopologicalSpace.PositiveCompacts.coe_mk
{α : Type u_1}
[TopologicalSpace α]
(s : Compacts α)
(h : (interior s.carrier).Nonempty)
:
theorem
TopologicalSpace.PositiveCompacts.carrier_eq_coe
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
s.carrier = ↑s
@[simp]
theorem
TopologicalSpace.PositiveCompacts.coe_toCompacts
{α : Type u_1}
[TopologicalSpace α]
(s : PositiveCompacts α)
:
↑s.toCompacts = ↑s
@[implicit_reducible]
instance
TopologicalSpace.PositiveCompacts.instMax
{α : Type u_1}
[TopologicalSpace α]
:
Max (PositiveCompacts α)
@[implicit_reducible]
instance
TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
Top (PositiveCompacts α)
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
@[simp]
theorem
TopologicalSpace.PositiveCompacts.coe_sup
{α : Type u_1}
[TopologicalSpace α]
(s t : PositiveCompacts α)
:
↑(s ⊔ t) = ↑s ∪ ↑t
@[simp]
theorem
TopologicalSpace.PositiveCompacts.coe_top
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
def
TopologicalSpace.PositiveCompacts.map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(hf' : IsOpenMap f)
(K : PositiveCompacts α)
:
The image of a positive compact set under a continuous open map.
Instances For
@[simp]
theorem
TopologicalSpace.PositiveCompacts.coe_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(hf' : IsOpenMap f)
(s : PositiveCompacts α)
:
↑(PositiveCompacts.map f hf hf' s) = f '' ↑s
@[simp]
theorem
TopologicalSpace.PositiveCompacts.map_id
{α : Type u_1}
[TopologicalSpace α]
(K : PositiveCompacts α)
:
PositiveCompacts.map id ⋯ ⋯ K = K
theorem
TopologicalSpace.PositiveCompacts.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
(f : β → γ)
(g : α → β)
(hf : Continuous f)
(hg : Continuous g)
(hf' : IsOpenMap f)
(hg' : IsOpenMap g)
(K : PositiveCompacts α)
:
PositiveCompacts.map (f ∘ g) ⋯ ⋯ K = PositiveCompacts.map f hf hf' (PositiveCompacts.map g hg hg' K)
theorem
exists_positiveCompacts_subset
{α : Type u_1}
[TopologicalSpace α]
[LocallyCompactSpace α]
{U : Set α}
(ho : IsOpen U)
(hn : U.Nonempty)
:
∃ (K : TopologicalSpace.PositiveCompacts α), ↑K ⊆ U
theorem
IsOpen.exists_positiveCompacts_closure_subset
{α : Type u_1}
[TopologicalSpace α]
[R1Space α]
[LocallyCompactSpace α]
{U : Set α}
(ho : IsOpen U)
(hn : U.Nonempty)
:
∃ (K : TopologicalSpace.PositiveCompacts α), closure ↑K ⊆ U
@[implicit_reducible]
instance
TopologicalSpace.PositiveCompacts.instInhabitedOfCompactSpaceOfNonempty
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[Nonempty α]
:
Inhabited (PositiveCompacts α)
instance
TopologicalSpace.PositiveCompacts.nonempty'
{α : Type u_1}
[TopologicalSpace α]
[WeaklyLocallyCompactSpace α]
[Nonempty α]
:
Nonempty (PositiveCompacts α)
In a nonempty locally compact space, there exists a compact set with nonempty interior.
@[implicit_reducible]
instance
TopologicalSpace.PositiveCompacts.instSProdProd
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
:
SProd (PositiveCompacts α) (PositiveCompacts β) (PositiveCompacts (α × β))
The product of two TopologicalSpace.PositiveCompacts, as a TopologicalSpace.PositiveCompacts
in the product space.
@[reducible, inline, deprecated "Use `K ×ˢ L` instead" (since := "2025-11-15")]
abbrev
TopologicalSpace.PositiveCompacts.prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : PositiveCompacts α)
(L : PositiveCompacts β)
:
PositiveCompacts (α × β)
The product of two TopologicalSpace.PositiveCompacts, as a TopologicalSpace.PositiveCompacts
in the product space.
Instances For
@[simp]
theorem
TopologicalSpace.PositiveCompacts.coe_prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : PositiveCompacts α)
(L : PositiveCompacts β)
:
Compact open sets #
structure
TopologicalSpace.CompactOpens
(α : Type u_4)
[TopologicalSpace α]
extends TopologicalSpace.Compacts α :
Type u_4
The type of compact open sets of a topological space. This is useful in non-Hausdorff contexts, in particular spectral spaces.
- isCompact' : IsCompact self.carrier
Instances For
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instSetLike
{α : Type u_1}
[TopologicalSpace α]
:
SetLike (CompactOpens α) α
@[implicit_reducible]
def
TopologicalSpace.CompactOpens.Simps.coe
{α : Type u_1}
[TopologicalSpace α]
(s : CompactOpens α)
:
Set α
See Note [custom simps projection].
Instances For
theorem
TopologicalSpace.CompactOpens.isCompact
{α : Type u_1}
[TopologicalSpace α]
(s : CompactOpens α)
:
IsCompact ↑s
theorem
TopologicalSpace.CompactOpens.isOpen
{α : Type u_1}
[TopologicalSpace α]
(s : CompactOpens α)
:
IsOpen ↑s
def
TopologicalSpace.CompactOpens.toOpens
{α : Type u_1}
[TopologicalSpace α]
(s : CompactOpens α)
:
Opens α
Reinterpret a compact open as an open.
Instances For
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_toOpens
{α : Type u_1}
[TopologicalSpace α]
(s : CompactOpens α)
:
↑s.toOpens = ↑s
def
TopologicalSpace.CompactOpens.toClopens
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : CompactOpens α)
:
Clopens α
Reinterpret a compact open as a clopen.
Instances For
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_toClopens
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s : CompactOpens α)
:
↑s.toClopens = ↑s
theorem
TopologicalSpace.CompactOpens.ext
{α : Type u_1}
[TopologicalSpace α]
{s t : CompactOpens α}
(h : ↑s = ↑t)
:
s = t
theorem
TopologicalSpace.CompactOpens.ext_iff
{α : Type u_1}
[TopologicalSpace α]
{s t : CompactOpens α}
:
s = t ↔ ↑s = ↑t
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_mk
{α : Type u_1}
[TopologicalSpace α]
(s : Compacts α)
(h : IsOpen s.carrier)
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instMax
{α : Type u_1}
[TopologicalSpace α]
:
Max (CompactOpens α)
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instBot
{α : Type u_1}
[TopologicalSpace α]
:
Bot (CompactOpens α)
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_sup
{α : Type u_1}
[TopologicalSpace α]
(s t : CompactOpens α)
:
↑(s ⊔ t) = ↑s ∪ ↑t
@[simp]
@[implicit_reducible]
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instOrderBot
{α : Type u_1}
[TopologicalSpace α]
:
OrderBot (CompactOpens α)
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_finsetSup
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_4}
{f : ι → CompactOpens α}
{s : Finset ι}
:
↑(s.sup f) = ⋃ i ∈ s, ↑(f i)
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instInhabited
{α : Type u_1}
[TopologicalSpace α]
:
Inhabited (CompactOpens α)
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instInf
{α : Type u_1}
[TopologicalSpace α]
[QuasiSeparatedSpace α]
:
Min (CompactOpens α)
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_inf
{α : Type u_1}
[TopologicalSpace α]
[QuasiSeparatedSpace α]
(s t : CompactOpens α)
:
↑(s ⊓ t) = ↑s ∩ ↑t
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instSemilatticeInf
{α : Type u_1}
[TopologicalSpace α]
[QuasiSeparatedSpace α]
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instSDiff
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
:
SDiff (CompactOpens α)
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_sdiff
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
(s t : CompactOpens α)
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instGeneralizedBooleanAlgebra
{α : Type u_1}
[TopologicalSpace α]
[T2Space α]
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instTop
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
:
Top (CompactOpens α)
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_top
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instBoundedOrder
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instCompl
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[T2Space α]
:
Compl (CompactOpens α)
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instHImp
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[T2Space α]
:
HImp (CompactOpens α)
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_compl
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[T2Space α]
(s : CompactOpens α)
:
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_himp
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[T2Space α]
(s t : CompactOpens α)
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instBooleanAlgebra
{α : Type u_1}
[TopologicalSpace α]
[CompactSpace α]
[T2Space α]
:
def
TopologicalSpace.CompactOpens.map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(hf' : IsOpenMap f)
(s : CompactOpens α)
:
The image of a compact open under a continuous open map.
Instances For
@[simp]
theorem
TopologicalSpace.CompactOpens.toCompacts_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(hf' : IsOpenMap f)
(s : CompactOpens α)
:
(map f hf hf' s).toCompacts = Compacts.map f hf s.toCompacts
@[deprecated TopologicalSpace.CompactOpens.toCompacts_map (since := "2025-11-13")]
theorem
TopologicalSpace.CompactOpens.map_toCompacts
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(f : α → β)
(hf : Continuous f)
(hf' : IsOpenMap f)
(s : CompactOpens α)
:
(map f hf hf' s).toCompacts = Compacts.map f hf s.toCompacts
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
(hf' : IsOpenMap f)
(s : CompactOpens α)
:
@[simp]
theorem
TopologicalSpace.CompactOpens.map_id
{α : Type u_1}
[TopologicalSpace α]
(K : CompactOpens α)
:
map id ⋯ ⋯ K = K
theorem
TopologicalSpace.CompactOpens.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
(f : β → γ)
(g : α → β)
(hf : Continuous f)
(hg : Continuous g)
(hf' : IsOpenMap f)
(hg' : IsOpenMap g)
(K : CompactOpens α)
:
@[implicit_reducible]
instance
TopologicalSpace.CompactOpens.instSProdProd
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
:
SProd (CompactOpens α) (CompactOpens β) (CompactOpens (α × β))
The product of two TopologicalSpace.CompactOpens, as a TopologicalSpace.CompactOpens in the
product space.
@[reducible, inline, deprecated "Use `K ×ˢ L` instead" (since := "2025-11-15")]
abbrev
TopologicalSpace.CompactOpens.prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : CompactOpens α)
(L : CompactOpens β)
:
CompactOpens (α × β)
The product of two TopologicalSpace.CompactOpens, as a TopologicalSpace.CompactOpens in the
product space.
Instances For
@[simp]
theorem
TopologicalSpace.CompactOpens.coe_prod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(K : CompactOpens α)
(L : CompactOpens β)
: