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) [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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance TopologicalSpace.Compacts.instPartialOrder {α : Type u_1} [TopologicalSpace α] : PartialOrder (Compacts α)

Equations

• TopologicalSpace.Compacts.instPartialOrder = PartialOrder.ofSetLike (TopologicalSpace.Compacts α) α

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

See Note [custom simps projection].

Equations

• TopologicalSpace.Compacts.Simps.coe s = ↑s

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.

Equations

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

@[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) : ↑{ carrier := s, isCompact' := h } = s

@[simp]

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

@[implicit_reducible]

instance TopologicalSpace.Compacts.instMax {α : Type u_1} [TopologicalSpace α] : Max (Compacts α)

Equations

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

@[implicit_reducible]

instance TopologicalSpace.Compacts.instMinOfT2Space {α : Type u_1} [TopologicalSpace α] [T2Space α] : Min (Compacts α)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• TopologicalSpace.Compacts.instOrderBot = { toBot := TopologicalSpace.Compacts.instBot, bot_le := ⋯ }

@[implicit_reducible]

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

Equations

• TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace = { toTop := TopologicalSpace.Compacts.instTopOfCompactSpace, le_top := ⋯, toOrderBot := TopologicalSpace.Compacts.instOrderBot }

@[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.

Equations

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

@[implicit_reducible]

instance TopologicalSpace.Compacts.instUniqueOfIsEmpty {α : Type u_1} [TopologicalSpace α] [IsEmpty α] : Unique (Compacts α)

Equations

• TopologicalSpace.Compacts.instUniqueOfIsEmpty = { toInhabited := TopologicalSpace.Compacts.instInhabited, uniq := ⋯ }

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

theorem TopologicalSpace.Compacts.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] : ↑⊤ = Set.univ

@[simp]

theorem TopologicalSpace.Compacts.coe_bot {α : Type u_1} [TopologicalSpace α] : ↑⊥ = ∅

@[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 α} : (↑s).Nonempty ↔ s ≠ ⊥

@[simp]

theorem TopologicalSpace.Compacts.coe_finset_sup {α : Type u_1} [TopologicalSpace α] {ι : Type u_4} {s : Finset ι} {f : ι → Compacts α} : ↑(s.sup f) = s.sup fun (i : ι) => ↑(f i)

@[implicit_reducible]

instance TopologicalSpace.Compacts.instSingleton {α : Type u_1} [TopologicalSpace α] : Singleton α (Compacts α)

Equations

• TopologicalSpace.Compacts.instSingleton = { singleton := fun (x : α) => { carrier := {x}, isCompact' := ⋯ } }

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

theorem TopologicalSpace.Compacts.disjoint_coe_iff {α : Type u_1} [TopologicalSpace α] (K L : Compacts α) : Disjoint ↑K ↑L ↔ Disjoint K L

instance TopologicalSpace.Compacts.instNontrivialOfNonempty {α : Type u_1} [TopologicalSpace α] [Nonempty α] : Nontrivial (Compacts α)

@[simp]

theorem TopologicalSpace.Compacts.subsingleton_iff {α : Type u_1} [TopologicalSpace α] : Subsingleton (Compacts α) ↔ IsEmpty α

@[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.

Equations

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

@[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) : Set.range (Compacts.map f ⋯) = {K : Compacts β | ↑K ⊆ Set.range f}

def TopologicalSpace.Compacts.equiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : Compacts α ≃ 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 := ⋯ }

@[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 β] : SProd (Compacts α) (Compacts β) (Compacts (α × β))

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

Equations

• TopologicalSpace.Compacts.instSProdProd = { sprod := fun (K : TopologicalSpace.Compacts α) (L : TopologicalSpace.Compacts β) => { carrier := ↑K ×ˢ ↑L, isCompact' := ⋯ } }

@[simp]

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

@[simp]

theorem TopologicalSpace.Compacts.toCloseds_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] [T2Space β] (K : Compacts α) (L : Compacts β) : (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds

@[simp]

theorem TopologicalSpace.Compacts.singleton_prod_singleton {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (x : α) (y : β) : {x} ×ˢ {y} = {(x, y)}

def TopologicalSpace.Compacts.compactNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : Set (Compacts α)

The compacts neigbourhoods of a compact

Equations

• K.compactNhds = {K' : TopologicalSpace.Compacts α | ∀ (x : ↥K), ↑K' ∈ nhds ↑x}

theorem TopologicalSpace.Compacts.subset_of_mem_compactNhds {α : Type u_1} [TopologicalSpace α] {K K' : Compacts α} (h : K' ∈ K.compactNhds) : ↑K ⊆ ↑K'

theorem TopologicalSpace.Compacts.exists_open_set_nhds_of_compactsNhds {α : Type u_1} [TopologicalSpace α] {K : Compacts α} (L : ↑K.compactNhds) : ∃ (U : Opens α), ↑K ⊆ ↑U ∧ ↑U ⊆ ↑↑L

theorem TopologicalSpace.Compacts.exists_open_set_nhds_of_mem_compactsNhds {α : Type u_1} [TopologicalSpace α] {K K' : Compacts α} (h : K' ∈ K.compactNhds) : ∃ (U : Opens α), ↑K ⊆ ↑U ∧ ↑U ⊆ ↑K'

def TopologicalSpace.Compacts.compactNhdsMkOfOpens {α : Type u_1} [TopologicalSpace α] {K : Compacts α} (L : Compacts α) (U : Opens α) (h1 : ↑K ⊆ ↑U) (h2 : ↑U ⊆ ↑L) : ↑K.compactNhds

The compact neigbourhood induced by the existence of an open subset between two compacts

Equations

• TopologicalSpace.Compacts.compactNhdsMkOfOpens L U h1 h2 = ⟨L, ⋯⟩

@[implicit_reducible]

instance TopologicalSpace.Compacts.instSemilatticeInfElemCompactNhdsOfT2Space {α : Type u_1} [TopologicalSpace α] [T2Space α] (K : Compacts α) : SemilatticeInf ↑K.compactNhds

Equations

• One or more equations did not get rendered due to their size.

def TopologicalSpace.Compacts.openNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : Set (Opens α)

The set of opens neighbourhood of a compact subset

Equations

• K.openNhds = {U : TopologicalSpace.Opens α | ↑K ⊆ ↑U}

instance TopologicalSpace.Compacts.instIsCodirectedOrderElemOpensOpenNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : IsCodirectedOrder ↑K.openNhds

@[implicit_reducible]

instance TopologicalSpace.Compacts.instTopElemOpensOpenNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : Top ↑K.openNhds

Equations

• K.instTopElemOpensOpenNhds = { top := ⟨⊤, ⋯⟩ }

@[implicit_reducible]

instance TopologicalSpace.Compacts.instBotElemOpensOpenNhdsBot {α : Type u_1} [TopologicalSpace α] : Bot ↑⊥.openNhds

Equations

• TopologicalSpace.Compacts.instBotElemOpensOpenNhdsBot = { bot := ⟨⊥, ⋯⟩ }

def TopologicalSpace.Compacts.openRcNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : Set (Opens α)

The opens neighbourhood of a compact subset that are relatively compact

Equations

• K.openRcNhds = {U : TopologicalSpace.Opens α | IsCompact (closure ↑U) ∧ ↑K ⊆ ↑U}

theorem TopologicalSpace.Compacts.subset_of_mem_openRcNhds {α : Type u_1} [TopologicalSpace α] {K : Compacts α} {U : Opens α} (h : U ∈ K.openRcNhds) : ↑K ⊆ ↑U

theorem TopologicalSpace.Compacts.isCompact_closure_of_mem_openRcNhds {α : Type u_1} [TopologicalSpace α] {K : Compacts α} {U : Opens α} (h : U ∈ K.openRcNhds) : IsCompact (closure ↑U)

theorem TopologicalSpace.Compacts.closure_mem_compactNhds_of_mem_openRcNhds {α : Type u_1} [TopologicalSpace α] {K : Compacts α} {U : Opens α} (h : U ∈ K.openRcNhds) : { carrier := closure ↑U, isCompact' := ⋯ } ∈ K.compactNhds

def TopologicalSpace.Compacts.openRcNhdsToOpenNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : ↑K.openRcNhds → ↑K.openNhds

The converting map from relatively compact opens neighbourhood of a compact subset to its opens neighbourhoods

Equations

• K.openRcNhdsToOpenNhds U = ⟨↑U, ⋯⟩

theorem TopologicalSpace.Compacts.openRcNhdsToOpenNhds_mono {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : Monotone K.openRcNhdsToOpenNhds

def TopologicalSpace.Compacts.openRcNhdsToCompactNhds {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : ↑K.openRcNhds → ↑K.compactNhds

An open relatively compact neighbourhood of K induces a compact neighbourhood by taking the closure

Equations

• K.openRcNhdsToCompactNhds U = ⟨{ carrier := closure ↑↑U, isCompact' := ⋯ }, ⋯⟩

theorem TopologicalSpace.Compacts.openRcNhdsToCompactNhds_mono {α : Type u_1} [TopologicalSpace α] (K : Compacts α) : Monotone K.openRcNhdsToCompactNhds

instance TopologicalSpace.Compacts.instIsCodirectedOrderElemOpensOpenRcNhdsOfT2Space {α : Type u_1} [TopologicalSpace α] [T2Space α] (K : Compacts α) : IsCodirectedOrder ↑K.openRcNhds

def TopologicalSpace.Opens.compactsInside {α : Type u_1} [TopologicalSpace α] (U : Opens α) : Set (Compacts α)

The set of compacts inside an open subset

Equations

• U.compactsInside = {K : TopologicalSpace.Compacts α | ↑K ⊆ ↑U}

def TopologicalSpace.Opens.openNhdsOfCompactsInside {α : Type u_1} [TopologicalSpace α] {U : Opens α} (K : ↑U.compactsInside) : ↑(↑K).openNhds

For K a compact subset insde an open subset U, U has a structure of open neighbourhood of K

Equations

• TopologicalSpace.Opens.openNhdsOfCompactsInside K = ⟨U, ⋯⟩

def TopologicalSpace.Compacts.compactsInsideOfOpenNhds {α : Type u_1} [TopologicalSpace α] {K : Compacts α} (U : ↑K.openNhds) : ↑(↑U).compactsInside

For U an open neighbourhood of K, K has a structure of compact insde U

Equations

• TopologicalSpace.Compacts.compactsInsideOfOpenNhds U = ⟨K, ⋯⟩

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.

• carrier : Set α
• isCompact' : IsCompact self.carrier
• nonempty' : self.carrier.Nonempty

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance TopologicalSpace.NonemptyCompacts.instPartialOrder {α : Type u_1} [TopologicalSpace α] : PartialOrder (NonemptyCompacts α)

Equations

• TopologicalSpace.NonemptyCompacts.instPartialOrder = PartialOrder.ofSetLike (TopologicalSpace.NonemptyCompacts α) α

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

See Note [custom simps projection].

Equations

• TopologicalSpace.NonemptyCompacts.Simps.coe s = ↑s

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.

Equations

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

@[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 α) : s.toCloseds = s.toCloseds

@[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) : ↑{ toCompacts := s, nonempty' := h } = ↑s

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 α)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty = { toTop := TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty, le_top := ⋯ }

@[simp]

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

@[simp]

theorem TopologicalSpace.NonemptyCompacts.toCompacts_sup {α : Type u_1} [TopologicalSpace α] (s t : NonemptyCompacts α) : (s ⊔ t).toCompacts = s.toCompacts ⊔ t.toCompacts

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [Nonempty α] : ↑⊤ = Set.univ

@[implicit_reducible]

instance TopologicalSpace.NonemptyCompacts.instSingleton {α : Type u_1} [TopologicalSpace α] : Singleton α (NonemptyCompacts α)

Equations

• TopologicalSpace.NonemptyCompacts.instSingleton = { singleton := fun (x : α) => { toCompacts := {x}, nonempty' := ⋯ } }

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_singleton {α : Type u_1} [TopologicalSpace α] (x : α) : ↑{x} = {x}

@[simp]

theorem TopologicalSpace.NonemptyCompacts.toCompacts_singleton {α : Type u_1} [TopologicalSpace α] (x : α) : {x}.toCompacts = {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.

Equations

• TopologicalSpace.NonemptyCompacts.instInhabited = { default := {default} }

instance TopologicalSpace.NonemptyCompacts.instIsEmpty {α : Type u_1} [TopologicalSpace α] [IsEmpty α] : IsEmpty (NonemptyCompacts α)

@[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 α] : Unique (NonemptyCompacts α)

Equations

• TopologicalSpace.NonemptyCompacts.instUnique = Unique.mk' (TopologicalSpace.NonemptyCompacts α)

instance TopologicalSpace.NonemptyCompacts.instNontrivial {α : Type u_1} [TopologicalSpace α] [Nontrivial α] : Nontrivial (NonemptyCompacts α)

@[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 α) : NonemptyCompacts β

The image of a nonempty compact set under a continuous function.

Equations

• TopologicalSpace.NonemptyCompacts.map f hf K = { toCompacts := TopologicalSpace.Compacts.map f hf K.toCompacts, nonempty' := ⋯ }

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem TopologicalSpace.NonemptyCompacts.toCompacts_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (K : NonemptyCompacts α) (L : NonemptyCompacts β) : (K ×ˢ L).toCompacts = K.toCompacts ×ˢ L.toCompacts

@[simp]

theorem TopologicalSpace.NonemptyCompacts.toCloseds_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] [T2Space β] (K : NonemptyCompacts α) (L : NonemptyCompacts β) : (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds

@[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.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance TopologicalSpace.PositiveCompacts.instPartialOrder {α : Type u_1} [TopologicalSpace α] : PartialOrder (PositiveCompacts α)

Equations

• TopologicalSpace.PositiveCompacts.instPartialOrder = PartialOrder.ofSetLike (TopologicalSpace.PositiveCompacts α) α

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

See Note [custom simps projection].

Equations

• TopologicalSpace.PositiveCompacts.Simps.coe s = ↑s

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

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

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

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

Reinterpret a positive compact as a nonempty compact.

Equations

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

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) : ↑{ toCompacts := s, interior_nonempty' := h } = ↑s

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 α)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty = { toTop := TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty, le_top := ⋯ }

@[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 α] : ↑⊤ = Set.univ

def TopologicalSpace.PositiveCompacts.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (K : PositiveCompacts α) : 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' := ⋯ }

@[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 α)

Equations

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance TopologicalSpace.CompactOpens.instPartialOrder {α : Type u_1} [TopologicalSpace α] : PartialOrder (CompactOpens α)

Equations

• TopologicalSpace.CompactOpens.instPartialOrder = PartialOrder.ofSetLike (TopologicalSpace.CompactOpens α) α

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

See Note [custom simps projection].

Equations

• TopologicalSpace.CompactOpens.Simps.coe s = ↑s

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.

Equations

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

@[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.

Equations

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

@[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) : ↑{ toCompacts := s, isOpen' := h } = ↑s

@[implicit_reducible]

instance TopologicalSpace.CompactOpens.instMax {α : Type u_1} [TopologicalSpace α] : Max (CompactOpens α)

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

@[simp]

theorem TopologicalSpace.CompactOpens.coe_bot {α : Type u_1} [TopologicalSpace α] : ↑⊥ = ∅

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• TopologicalSpace.CompactOpens.instOrderBot = { toBot := TopologicalSpace.CompactOpens.instBot, bot_le := ⋯ }

@[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 α)

Equations

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

@[implicit_reducible]

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

Equations

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

@[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 α] : SemilatticeInf (CompactOpens α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

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

@[simp]

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

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

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

@[simp]

theorem TopologicalSpace.CompactOpens.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] : ↑⊤ = Set.univ

@[implicit_reducible]

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

Equations

• TopologicalSpace.CompactOpens.instBoundedOrder = { toTop := TopologicalSpace.CompactOpens.instTop, le_top := ⋯, toOrderBot := TopologicalSpace.CompactOpens.instOrderBot }

@[implicit_reducible]

instance TopologicalSpace.CompactOpens.instCompl {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] : Compl (CompactOpens α)

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

def TopologicalSpace.CompactOpens.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (s : CompactOpens α) : 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' := ⋯ }

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

@[simp]

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

@[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 α) : map (f ∘ g) ⋯ ⋯ K = map f hf hf' (map g hg hg' K)

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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