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 #

source

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

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

source

theorem TopologicalSpace.Compacts.isCompact' {α : Type u_4} [TopologicalSpace α] (self : TopologicalSpace.Compacts α) :

IsCompact self.carrier

source

instance TopologicalSpace.Compacts.instSetLike {α : Type u_1} [TopologicalSpace α] :

SetLike (TopologicalSpace.Compacts α) α

Equations

TopologicalSpace.Compacts.instSetLike = { coe := TopologicalSpace.Compacts.carrier, coe_injective' := ⋯ }

source

def TopologicalSpace.Compacts.Simps.coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) :

Set α

See Note [custom simps projection].

Equations

TopologicalSpace.Compacts.Simps.coe s = ↑s

source

theorem TopologicalSpace.Compacts.isCompact {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) :

IsCompact ↑s

source

instance TopologicalSpace.Compacts.instCompactSpaceSubtypeMem {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.Compacts α) :

CompactSpace { x : α // x ∈ K }

Equations

⋯ = ⋯

source

instance TopologicalSpace.Compacts.instCanLiftSetCoeIsCompact {α : Type u_1} [TopologicalSpace α] :

CanLift (Set α) (TopologicalSpace.Compacts α) SetLike.coe IsCompact

Equations

⋯ = ⋯

source

theorem TopologicalSpace.Compacts.ext_iff {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.Compacts α} {t : TopologicalSpace.Compacts α} :

s = t ↔ ↑s = ↑t

source

theorem TopologicalSpace.Compacts.ext {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.Compacts α} {t : TopologicalSpace.Compacts α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem TopologicalSpace.Compacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : Set α) (h : IsCompact s) :

↑{ carrier := s, isCompact' := h } = s

source

@[simp]

theorem TopologicalSpace.Compacts.carrier_eq_coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) :

s.carrier = ↑s

source

instance TopologicalSpace.Compacts.instSup {α : Type u_1} [TopologicalSpace α] :

Sup (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instSup = { sup := fun (s t : TopologicalSpace.Compacts α) => { carrier := ↑s ∪ ↑t, isCompact' := ⋯ } }

source

instance TopologicalSpace.Compacts.instInfOfT2Space {α : Type u_1} [TopologicalSpace α] [T2Space α] :

Inf (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instInfOfT2Space = { inf := fun (s t : TopologicalSpace.Compacts α) => { carrier := ↑s ∩ ↑t, isCompact' := ⋯ } }

source

instance TopologicalSpace.Compacts.instTopOfCompactSpace {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :

Top (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instTopOfCompactSpace = { top := { carrier := Set.univ, isCompact' := ⋯ } }

source

instance TopologicalSpace.Compacts.instBot {α : Type u_1} [TopologicalSpace α] :

Bot (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instBot = { bot := { carrier := ∅, isCompact' := ⋯ } }

source

instance TopologicalSpace.Compacts.instSemilatticeSup {α : Type u_1} [TopologicalSpace α] :

SemilatticeSup (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instSemilatticeSup = Function.Injective.semilatticeSup SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.Compacts.instDistribLatticeOfT2Space {α : Type u_1} [TopologicalSpace α] [T2Space α] :

DistribLattice (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instDistribLatticeOfT2Space = Function.Injective.distribLattice SetLike.coe ⋯ ⋯ ⋯

source

instance TopologicalSpace.Compacts.instOrderBot {α : Type u_1} [TopologicalSpace α] :

OrderBot (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instOrderBot = OrderBot.lift SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :

BoundedOrder (TopologicalSpace.Compacts α)

Equations

TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace = BoundedOrder.lift SetLike.coe ⋯ ⋯ ⋯

source

instance TopologicalSpace.Compacts.instInhabited {α : Type u_1} [TopologicalSpace α] :

Inhabited (TopologicalSpace.Compacts α)

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

Equations

TopologicalSpace.Compacts.instInhabited = { default := ⊥ }

source

@[simp]

theorem TopologicalSpace.Compacts.coe_sup {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (t : TopologicalSpace.Compacts α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

theorem TopologicalSpace.Compacts.coe_inf {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.Compacts α) (t : TopologicalSpace.Compacts α) :

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

theorem TopologicalSpace.Compacts.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :

↑⊤ = Set.univ

source

@[simp]

theorem TopologicalSpace.Compacts.coe_bot {α : Type u_1} [TopologicalSpace α] :

↑⊥ = ∅

source

@[simp]

theorem TopologicalSpace.Compacts.coe_finset_sup {α : Type u_1} [TopologicalSpace α] {ι : Type u_4} {s : Finset ι} {f : ι → TopologicalSpace.Compacts α} :

↑(s.sup f) = s.sup fun (i : ι) => ↑(f i)

source

def TopologicalSpace.Compacts.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (K : TopologicalSpace.Compacts α) :

TopologicalSpace.Compacts β

The image of a compact set under a continuous function.

Equations

TopologicalSpace.Compacts.map f hf K = { carrier := f '' K.carrier, isCompact' := ⋯ }

source

@[simp]

theorem TopologicalSpace.Compacts.coe_map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (s : TopologicalSpace.Compacts α) :

↑(TopologicalSpace.Compacts.map f hf s) = f '' ↑s

source

@[simp]

theorem TopologicalSpace.Compacts.map_id {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.Compacts α) :

TopologicalSpace.Compacts.map id ⋯ K = K

source

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 : TopologicalSpace.Compacts α) :

TopologicalSpace.Compacts.map (f ∘ g) ⋯ K = TopologicalSpace.Compacts.map f hf (TopologicalSpace.Compacts.map g hg K)

source

@[simp]

theorem TopologicalSpace.Compacts.equiv_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) (K : TopologicalSpace.Compacts β) :

(TopologicalSpace.Compacts.equiv f).symm K = TopologicalSpace.Compacts.map ⇑f.symm ⋯ K

source

@[simp]

theorem TopologicalSpace.Compacts.equiv_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) (K : TopologicalSpace.Compacts α) :

(TopologicalSpace.Compacts.equiv f) K = TopologicalSpace.Compacts.map ⇑f ⋯ K

source

def TopologicalSpace.Compacts.equiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :

TopologicalSpace.Compacts α ≃ TopologicalSpace.Compacts β

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

Equations

TopologicalSpace.Compacts.equiv f = { toFun := TopologicalSpace.Compacts.map ⇑f ⋯, invFun := TopologicalSpace.Compacts.map ⇑f.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem TopologicalSpace.Compacts.equiv_refl {α : Type u_1} [TopologicalSpace α] :

TopologicalSpace.Compacts.equiv (Homeomorph.refl α) = Equiv.refl (TopologicalSpace.Compacts α)

source

@[simp]

theorem TopologicalSpace.Compacts.equiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) :

TopologicalSpace.Compacts.equiv (f.trans g) = (TopologicalSpace.Compacts.equiv f).trans (TopologicalSpace.Compacts.equiv g)

source

@[simp]

theorem TopologicalSpace.Compacts.equiv_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :

TopologicalSpace.Compacts.equiv f.symm = (TopologicalSpace.Compacts.equiv f).symm

source

theorem TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) (K : TopologicalSpace.Compacts α) :

↑((TopologicalSpace.Compacts.equiv f) K) = ⇑f.symm ⁻¹' ↑K

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

source

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

TopologicalSpace.Compacts (α × β)

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

Equations

K.prod L = { carrier := ↑K ×ˢ ↑L, isCompact' := ⋯ }

source

@[simp]

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

↑(K.prod L) = ↑K ×ˢ ↑L

Nonempty compact sets #

source

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

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

source

theorem TopologicalSpace.NonemptyCompacts.nonempty' {α : Type u_4} [TopologicalSpace α] (self : TopologicalSpace.NonemptyCompacts α) :

self.carrier.Nonempty

source

instance TopologicalSpace.NonemptyCompacts.instSetLike {α : Type u_1} [TopologicalSpace α] :

SetLike (TopologicalSpace.NonemptyCompacts α) α

Equations

TopologicalSpace.NonemptyCompacts.instSetLike = { coe := fun (s : TopologicalSpace.NonemptyCompacts α) => s.carrier, coe_injective' := ⋯ }

source

def TopologicalSpace.NonemptyCompacts.Simps.coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α) :

Set α

See Note [custom simps projection].

Equations

TopologicalSpace.NonemptyCompacts.Simps.coe s = ↑s

source

theorem TopologicalSpace.NonemptyCompacts.isCompact {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α) :

IsCompact ↑s

source

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

(↑s).Nonempty

source

def TopologicalSpace.NonemptyCompacts.toCloseds {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.NonemptyCompacts α) :

TopologicalSpace.Closeds α

Reinterpret a nonempty compact as a closed set.

Equations

s.toCloseds = { carrier := ↑s, closed' := ⋯ }

source

theorem TopologicalSpace.NonemptyCompacts.ext_iff {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.NonemptyCompacts α} {t : TopologicalSpace.NonemptyCompacts α} :

s = t ↔ ↑s = ↑t

source

theorem TopologicalSpace.NonemptyCompacts.ext {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.NonemptyCompacts α} {t : TopologicalSpace.NonemptyCompacts α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : s.carrier.Nonempty) :

↑{ toCompacts := s, nonempty' := h } = ↑s

source

theorem TopologicalSpace.NonemptyCompacts.carrier_eq_coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α) :

s.carrier = ↑s

source

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_toCompacts {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α) :

↑s.toCompacts = ↑s

source

instance TopologicalSpace.NonemptyCompacts.instSup {α : Type u_1} [TopologicalSpace α] :

Sup (TopologicalSpace.NonemptyCompacts α)

Equations

TopologicalSpace.NonemptyCompacts.instSup = { sup := fun (s t : TopologicalSpace.NonemptyCompacts α) => { toCompacts := s.toCompacts ⊔ t.toCompacts, nonempty' := ⋯ } }

source

instance TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

Top (TopologicalSpace.NonemptyCompacts α)

Equations

TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty = { top := { toCompacts := ⊤, nonempty' := ⋯ } }

source

instance TopologicalSpace.NonemptyCompacts.instSemilatticeSup {α : Type u_1} [TopologicalSpace α] :

SemilatticeSup (TopologicalSpace.NonemptyCompacts α)

Equations

TopologicalSpace.NonemptyCompacts.instSemilatticeSup = Function.Injective.semilatticeSup SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

OrderTop (TopologicalSpace.NonemptyCompacts α)

Equations

TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty = OrderTop.lift SetLike.coe ⋯ ⋯

source

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_sup {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α) (t : TopologicalSpace.NonemptyCompacts α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

↑⊤ = Set.univ

source

instance TopologicalSpace.NonemptyCompacts.instInhabited {α : Type u_1} [TopologicalSpace α] [Inhabited α] :

Inhabited (TopologicalSpace.NonemptyCompacts α)

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' := ⋯ } }

source

instance TopologicalSpace.NonemptyCompacts.toCompactSpace {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.NonemptyCompacts α} :

CompactSpace { x : α // x ∈ s }

Equations

⋯ = ⋯

source

instance TopologicalSpace.NonemptyCompacts.toNonempty {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.NonemptyCompacts α} :

Nonempty { x : α // x ∈ s }

Equations

⋯ = ⋯

source

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

TopologicalSpace.NonemptyCompacts (α × β)

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

Equations

K.prod L = { toCompacts := K.prod L.toCompacts, nonempty' := ⋯ }

source

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (K : TopologicalSpace.NonemptyCompacts α) (L : TopologicalSpace.NonemptyCompacts β) :

↑(K.prod L) = ↑K ×ˢ ↑L

Positive compact sets #

source

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.

carrier : Set α
isCompact' : IsCompact self.carrier
interior_nonempty' : (interior self.carrier).Nonempty

Instances For

source

theorem TopologicalSpace.PositiveCompacts.interior_nonempty' {α : Type u_4} [TopologicalSpace α] (self : TopologicalSpace.PositiveCompacts α) :

(interior self.carrier).Nonempty

source

instance TopologicalSpace.PositiveCompacts.instSetLike {α : Type u_1} [TopologicalSpace α] :

SetLike (TopologicalSpace.PositiveCompacts α) α

Equations

TopologicalSpace.PositiveCompacts.instSetLike = { coe := fun (s : TopologicalSpace.PositiveCompacts α) => s.carrier, coe_injective' := ⋯ }

source

def TopologicalSpace.PositiveCompacts.Simps.coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) :

Set α

See Note [custom simps projection].

Equations

TopologicalSpace.PositiveCompacts.Simps.coe s = ↑s

source

theorem TopologicalSpace.PositiveCompacts.isCompact {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) :

IsCompact ↑s

source

theorem TopologicalSpace.PositiveCompacts.interior_nonempty {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) :

(interior ↑s).Nonempty

source

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

(↑s).Nonempty

source

def TopologicalSpace.PositiveCompacts.toNonemptyCompacts {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) :

TopologicalSpace.NonemptyCompacts α

Reinterpret a positive compact as a nonempty compact.

Equations

s.toNonemptyCompacts = { toCompacts := s.toCompacts, nonempty' := ⋯ }

source

theorem TopologicalSpace.PositiveCompacts.ext_iff {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.PositiveCompacts α} {t : TopologicalSpace.PositiveCompacts α} :

s = t ↔ ↑s = ↑t

source

theorem TopologicalSpace.PositiveCompacts.ext {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.PositiveCompacts α} {t : TopologicalSpace.PositiveCompacts α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : (interior s.carrier).Nonempty) :

↑{ toCompacts := s, interior_nonempty' := h } = ↑s

source

theorem TopologicalSpace.PositiveCompacts.carrier_eq_coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) :

s.carrier = ↑s

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_toCompacts {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) :

↑s.toCompacts = ↑s

source

instance TopologicalSpace.PositiveCompacts.instSup {α : Type u_1} [TopologicalSpace α] :

Sup (TopologicalSpace.PositiveCompacts α)

Equations

TopologicalSpace.PositiveCompacts.instSup = { sup := fun (s t : TopologicalSpace.PositiveCompacts α) => { toCompacts := s.toCompacts ⊔ t.toCompacts, interior_nonempty' := ⋯ } }

source

instance TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

Top (TopologicalSpace.PositiveCompacts α)

Equations

TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty = { top := { toCompacts := ⊤, interior_nonempty' := ⋯ } }

source

instance TopologicalSpace.PositiveCompacts.instSemilatticeSup {α : Type u_1} [TopologicalSpace α] :

SemilatticeSup (TopologicalSpace.PositiveCompacts α)

Equations

TopologicalSpace.PositiveCompacts.instSemilatticeSup = Function.Injective.semilatticeSup SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

OrderTop (TopologicalSpace.PositiveCompacts α)

Equations

TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty = OrderTop.lift SetLike.coe ⋯ ⋯

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_sup {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) (t : TopologicalSpace.PositiveCompacts α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

↑⊤ = Set.univ

source

def TopologicalSpace.PositiveCompacts.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (K : TopologicalSpace.PositiveCompacts α) :

TopologicalSpace.PositiveCompacts β

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

Equations

TopologicalSpace.PositiveCompacts.map f hf hf' K = { toCompacts := TopologicalSpace.Compacts.map f hf K.toCompacts, interior_nonempty' := ⋯ }

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.PositiveCompacts α) :

↑(TopologicalSpace.PositiveCompacts.map f hf hf' s) = f '' ↑s

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.map_id {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.PositiveCompacts α) :

TopologicalSpace.PositiveCompacts.map id ⋯ ⋯ K = K

source

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 : TopologicalSpace.PositiveCompacts α) :

TopologicalSpace.PositiveCompacts.map (f ∘ g) ⋯ ⋯ K = TopologicalSpace.PositiveCompacts.map f hf hf' (TopologicalSpace.PositiveCompacts.map g hg hg' K)

source

theorem exists_positiveCompacts_subset {α : Type u_1} [TopologicalSpace α] [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : U.Nonempty) :

∃ (K : TopologicalSpace.PositiveCompacts α), ↑K ⊆ U

source

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

source

instance TopologicalSpace.PositiveCompacts.instInhabitedOfCompactSpaceOfNonempty {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] :

Inhabited (TopologicalSpace.PositiveCompacts α)

Equations

TopologicalSpace.PositiveCompacts.instInhabitedOfCompactSpaceOfNonempty = { default := ⊤ }

source

instance TopologicalSpace.PositiveCompacts.nonempty' {α : Type u_1} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [Nonempty α] :

Nonempty (TopologicalSpace.PositiveCompacts α)

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

Equations

⋯ = ⋯

source

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

TopologicalSpace.PositiveCompacts (α × β)

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' := ⋯ }

source

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (K : TopologicalSpace.PositiveCompacts α) (L : TopologicalSpace.PositiveCompacts β) :

↑(K.prod L) = ↑K ×ˢ ↑L

Compact open sets #

source

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.

carrier : Set α
isCompact' : IsCompact self.carrier
isOpen' : IsOpen self.carrier

Instances For

source

theorem TopologicalSpace.CompactOpens.isOpen' {α : Type u_4} [TopologicalSpace α] (self : TopologicalSpace.CompactOpens α) :

IsOpen self.carrier

source

instance TopologicalSpace.CompactOpens.instSetLike {α : Type u_1} [TopologicalSpace α] :

SetLike (TopologicalSpace.CompactOpens α) α

Equations

TopologicalSpace.CompactOpens.instSetLike = { coe := fun (s : TopologicalSpace.CompactOpens α) => s.carrier, coe_injective' := ⋯ }

source

def TopologicalSpace.CompactOpens.Simps.coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.CompactOpens α) :

Set α

See Note [custom simps projection].

Equations

TopologicalSpace.CompactOpens.Simps.coe s = ↑s

source

theorem TopologicalSpace.CompactOpens.isCompact {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.CompactOpens α) :

IsCompact ↑s

source

theorem TopologicalSpace.CompactOpens.isOpen {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.CompactOpens α) :

IsOpen ↑s

source

@[simp]

theorem TopologicalSpace.CompactOpens.toOpens_coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.CompactOpens α) :

↑s.toOpens = ↑s

source

def TopologicalSpace.CompactOpens.toOpens {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.CompactOpens α) :

TopologicalSpace.Opens α

Reinterpret a compact open as an open.

Equations

s.toOpens = { carrier := ↑s, is_open' := ⋯ }

source

@[simp]

theorem TopologicalSpace.CompactOpens.toClopens_coe {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) :

↑s.toClopens = ↑s

source

def TopologicalSpace.CompactOpens.toClopens {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) :

TopologicalSpace.Clopens α

Reinterpret a compact open as a clopen.

Equations

s.toClopens = { carrier := ↑s, isClopen' := ⋯ }

source

theorem TopologicalSpace.CompactOpens.ext_iff {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.CompactOpens α} {t : TopologicalSpace.CompactOpens α} :

s = t ↔ ↑s = ↑t

source

theorem TopologicalSpace.CompactOpens.ext {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.CompactOpens α} {t : TopologicalSpace.CompactOpens α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : IsOpen s.carrier) :

↑{ toCompacts := s, isOpen' := h } = ↑s

source

instance TopologicalSpace.CompactOpens.instSup {α : Type u_1} [TopologicalSpace α] :

Sup (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instSup = { sup := fun (s t : TopologicalSpace.CompactOpens α) => { toCompacts := s.toCompacts ⊔ t.toCompacts, isOpen' := ⋯ } }

source

instance TopologicalSpace.CompactOpens.instBot {α : Type u_1} [TopologicalSpace α] :

Bot (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instBot = { bot := { toCompacts := ⊥, isOpen' := ⋯ } }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_sup {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.CompactOpens α) (t : TopologicalSpace.CompactOpens α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_bot {α : Type u_1} [TopologicalSpace α] :

↑⊥ = ∅

source

instance TopologicalSpace.CompactOpens.instSemilatticeSup {α : Type u_1} [TopologicalSpace α] :

SemilatticeSup (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instSemilatticeSup = Function.Injective.semilatticeSup SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.CompactOpens.instOrderBot {α : Type u_1} [TopologicalSpace α] :

OrderBot (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instOrderBot = OrderBot.lift SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.CompactOpens.instInhabited {α : Type u_1} [TopologicalSpace α] :

Inhabited (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instInhabited = { default := ⊥ }

source

instance TopologicalSpace.CompactOpens.instInf {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] :

Inf (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instInf = { inf := fun (U V : TopologicalSpace.CompactOpens α) => { carrier := ↑U ∩ ↑V, isCompact' := ⋯, isOpen' := ⋯ } }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_inf {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] (s : TopologicalSpace.CompactOpens α) (t : TopologicalSpace.CompactOpens α) :

↑(s ⊓ t) = ↑s ∩ ↑t

source

instance TopologicalSpace.CompactOpens.instSemilatticeInf {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] :

SemilatticeInf (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instSemilatticeInf = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯

source

instance TopologicalSpace.CompactOpens.instSDiff {α : Type u_1} [TopologicalSpace α] [T2Space α] :

SDiff (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instSDiff = { sdiff := fun (s t : TopologicalSpace.CompactOpens α) => { carrier := ↑s \ ↑t, isCompact' := ⋯, isOpen' := ⋯ } }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_sdiff {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) (t : TopologicalSpace.CompactOpens α) :

↑(s \ t) = ↑s \ ↑t

source

instance TopologicalSpace.CompactOpens.instGeneralizedBooleanAlgebra {α : Type u_1} [TopologicalSpace α] [T2Space α] :

GeneralizedBooleanAlgebra (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instGeneralizedBooleanAlgebra = Function.Injective.generalizedBooleanAlgebra SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

source

instance TopologicalSpace.CompactOpens.instTop {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :

Top (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instTop = { top := { toCompacts := ⊤, isOpen' := ⋯ } }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :

↑⊤ = Set.univ

source

instance TopologicalSpace.CompactOpens.instBoundedOrder {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :

BoundedOrder (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instBoundedOrder = BoundedOrder.lift SetLike.coe ⋯ ⋯ ⋯

source

instance TopologicalSpace.CompactOpens.instHasCompl {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] :

HasCompl (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instHasCompl = { compl := fun (s : TopologicalSpace.CompactOpens α) => { carrier := (↑s)ᶜ, isCompact' := ⋯, isOpen' := ⋯ } }

source

instance TopologicalSpace.CompactOpens.instHImp {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] :

HImp (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instHImp = { himp := fun (s t : TopologicalSpace.CompactOpens α) => { carrier := ↑s ⇨ ↑t, isCompact' := ⋯, isOpen' := ⋯ } }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_compl {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) :

↑sᶜ = (↑s)ᶜ

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_himp {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) (t : TopologicalSpace.CompactOpens α) :

↑(s ⇨ t) = ↑s ⇨ ↑t

source

instance TopologicalSpace.CompactOpens.instBooleanAlgebra {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] :

BooleanAlgebra (TopologicalSpace.CompactOpens α)

Equations

TopologicalSpace.CompactOpens.instBooleanAlgebra = Function.Injective.booleanAlgebra SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

@[simp]

theorem TopologicalSpace.CompactOpens.map_toCompacts {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α) :

(TopologicalSpace.CompactOpens.map f hf hf' s).toCompacts = TopologicalSpace.Compacts.map f hf s.toCompacts

source

def TopologicalSpace.CompactOpens.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α) :

TopologicalSpace.CompactOpens β

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

Equations

TopologicalSpace.CompactOpens.map f hf hf' s = { toCompacts := TopologicalSpace.Compacts.map f hf s.toCompacts, isOpen' := ⋯ }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α) :

↑(TopologicalSpace.CompactOpens.map f hf hf' s) = f '' ↑s

source

@[simp]

theorem TopologicalSpace.CompactOpens.map_id {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.CompactOpens α) :

TopologicalSpace.CompactOpens.map id ⋯ ⋯ K = K

source

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 : TopologicalSpace.CompactOpens α) :

TopologicalSpace.CompactOpens.map (f ∘ g) ⋯ ⋯ K = TopologicalSpace.CompactOpens.map f hf hf' (TopologicalSpace.CompactOpens.map g hg hg' K)

source

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

TopologicalSpace.CompactOpens (α × β)

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

Equations

K.prod L = { toCompacts := K.prod L.toCompacts, isOpen' := ⋯ }

source

@[simp]

theorem TopologicalSpace.CompactOpens.coe_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (K : TopologicalSpace.CompactOpens α) (L : TopologicalSpace.CompactOpens β) :

↑(K.prod L) = ↑K ×ˢ ↑L

Documentation

Mathlib.Topology.Sets.Compacts

Compact sets #

Main Definitions #

Compact sets #

Nonempty compact sets #

Positive compact sets #

Compact open sets #