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 α
• isCompact' : IsCompact self.carrier

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

Equations

• TopologicalSpace.Compacts.instSetLikeCompacts = { coe := TopologicalSpace.Compacts.carrier, coe_injective' := (_ : ∀ (s t : TopologicalSpace.Compacts α), s.carrier = t.carrier → s = t) }

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

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

instance TopologicalSpace.Compacts.instCompactSpaceSubtypeMemCompactsInstMembershipInstSetLikeCompactsInstTopologicalSpaceSubtype {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.Compacts α) : CompactSpace ↥K

Equations

• (_ : CompactSpace ↥K) = (_ : CompactSpace ↑↑K)

instance TopologicalSpace.Compacts.instCanLiftSetCompactsCoeInstSetLikeCompactsIsCompact {α : Type u_1} [TopologicalSpace α] : CanLift (Set α) (TopologicalSpace.Compacts α) SetLike.coe IsCompact

Equations

• (_ : CanLift (Set α) (TopologicalSpace.Compacts α) SetLike.coe IsCompact) = (_ : CanLift (Set α) (TopologicalSpace.Compacts α) SetLike.coe IsCompact)

theorem TopologicalSpace.Compacts.ext {α : Type u_1} [TopologicalSpace α] {s : TopologicalSpace.Compacts α} {t : TopologicalSpace.Compacts α} (h : ↑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 : TopologicalSpace.Compacts α) : s.carrier = ↑s

instance TopologicalSpace.Compacts.instSupCompacts {α : Type u_1} [TopologicalSpace α] : Sup (TopologicalSpace.Compacts α)

Equations

• TopologicalSpace.Compacts.instSupCompacts = { sup := fun (s t : TopologicalSpace.Compacts α) => { carrier := ↑s ∪ ↑t, isCompact' := (_ : IsCompact (↑s ∪ ↑t)) } }

instance TopologicalSpace.Compacts.instInfCompacts {α : Type u_1} [TopologicalSpace α] [T2Space α] : Inf (TopologicalSpace.Compacts α)

Equations

• TopologicalSpace.Compacts.instInfCompacts = { inf := fun (s t : TopologicalSpace.Compacts α) => { carrier := ↑s ∩ ↑t, isCompact' := (_ : IsCompact (↑s ∩ ↑t)) } }

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

Equations

• TopologicalSpace.Compacts.instTopCompacts = { top := { carrier := Set.univ, isCompact' := (_ : IsCompact Set.univ) } }

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

Equations

• TopologicalSpace.Compacts.instBotCompacts = { bot := { carrier := ∅, isCompact' := (_ : IsCompact ∅) } }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance TopologicalSpace.Compacts.instInhabitedCompacts {α : Type u_1} [TopologicalSpace α] : Inhabited (TopologicalSpace.Compacts α)

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

Equations

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

@[simp]

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

@[simp]

theorem TopologicalSpace.Compacts.coe_inf {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.Compacts α) (t : TopologicalSpace.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_finset_sup {α : Type u_1} [TopologicalSpace α] {ι : Type u_4} {s : Finset ι} {f : ι → TopologicalSpace.Compacts α} : ↑(Finset.sup s f) = Finset.sup s fun (i : ι) => ↑(f i)

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' := (_ : IsCompact (f '' K.carrier)) }

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

@[simp]

theorem TopologicalSpace.Compacts.map_id {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.Compacts α) : TopologicalSpace.Compacts.map id (_ : Continuous 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 : TopologicalSpace.Compacts α) : TopologicalSpace.Compacts.map (f ∘ g) (_ : Continuous (f ∘ g)) K = TopologicalSpace.Compacts.map f hf (TopologicalSpace.Compacts.map g hg K)

@[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 (_ : Continuous ⇑f) K

@[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 ⇑(Homeomorph.symm f) (_ : Continuous ⇑(Homeomorph.symm f)) K

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

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

@[simp]

theorem TopologicalSpace.Compacts.equiv_refl {α : Type u_1} [TopologicalSpace α] : TopologicalSpace.Compacts.equiv (Homeomorph.refl α) = Equiv.refl (TopologicalSpace.Compacts α)

@[simp]

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

@[simp]

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

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) = ⇑(Homeomorph.symm f) ⁻¹' ↑K

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

def TopologicalSpace.Compacts.prod {α : Type u_1} {β : Type u_2} [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

• TopologicalSpace.Compacts.prod K L = { carrier := ↑K ×ˢ ↑L, isCompact' := (_ : IsCompact (↑K ×ˢ ↑L)) }

@[simp]

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

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' : Set.Nonempty self.carrier

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

Equations

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

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

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

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

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

Reinterpret a nonempty compact as a closed set.

Equations

• TopologicalSpace.NonemptyCompacts.toCloseds s = { carrier := ↑s, closed' := (_ : IsClosed ↑s) }

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

@[simp]

theorem TopologicalSpace.NonemptyCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : Set.Nonempty s.carrier) : ↑{ toCompacts := s, nonempty' := h } = ↑s

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

@[simp]

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

instance TopologicalSpace.NonemptyCompacts.instSupNonemptyCompacts {α : Type u_1} [TopologicalSpace α] : Sup (TopologicalSpace.NonemptyCompacts α)

Equations

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

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

Equations

• TopologicalSpace.NonemptyCompacts.instTopNonemptyCompacts = { top := { toCompacts := ⊤, nonempty' := (_ : Set.Nonempty Set.univ) } }

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

instance TopologicalSpace.NonemptyCompacts.instInhabitedNonemptyCompacts {α : 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

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

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

Equations

• (_ : CompactSpace ↥s) = (_ : CompactSpace ↑↑s)

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

Equations

• (_ : Nonempty ↥s) = (_ : Nonempty ↑↑s)

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

• TopologicalSpace.NonemptyCompacts.prod K L = let src := TopologicalSpace.Compacts.prod K.toCompacts L.toCompacts; { toCompacts := src, nonempty' := (_ : Set.Nonempty (↑K ×ˢ ↑L.toCompacts)) }

@[simp]

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

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' : Set.Nonempty (interior self.carrier)

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

Equations

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

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

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

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

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

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

Reinterpret a positive compact as a nonempty compact.

Equations

• TopologicalSpace.PositiveCompacts.toNonemptyCompacts s = { toCompacts := s.toCompacts, nonempty' := (_ : Set.Nonempty ↑s) }

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

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : Set.Nonempty (interior s.carrier)) : ↑{ toCompacts := s, interior_nonempty' := h } = ↑s

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

@[simp]

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

instance TopologicalSpace.PositiveCompacts.instSupPositiveCompacts {α : Type u_1} [TopologicalSpace α] : Sup (TopologicalSpace.PositiveCompacts α)

Equations

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

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

Equations

• TopologicalSpace.PositiveCompacts.instTopPositiveCompacts = { top := { toCompacts := ⊤, interior_nonempty' := (_ : Set.Nonempty (interior Set.univ)) } }

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

Equations

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

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

Equations

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

@[simp]

theorem TopologicalSpace.PositiveCompacts.coe_sup {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α) (t : TopologicalSpace.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 : TopologicalSpace.PositiveCompacts α) : TopologicalSpace.PositiveCompacts β

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

Equations

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

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

@[simp]

theorem TopologicalSpace.PositiveCompacts.map_id {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.PositiveCompacts α) : TopologicalSpace.PositiveCompacts.map id (_ : Continuous id) (_ : IsOpenMap 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 : TopologicalSpace.PositiveCompacts α) : TopologicalSpace.PositiveCompacts.map (f ∘ g) (_ : Continuous (f ∘ g)) (_ : IsOpenMap (f ∘ g)) K = TopologicalSpace.PositiveCompacts.map f hf hf' (TopologicalSpace.PositiveCompacts.map g hg hg' K)

theorem exists_positiveCompacts_subset {α : Type u_1} [TopologicalSpace α] [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : Set.Nonempty U) : ∃ (K : TopologicalSpace.PositiveCompacts α), ↑K ⊆ U

theorem IsOpen.exists_positiveCompacts_closure_subset {α : Type u_1} [TopologicalSpace α] [R1Space α] [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : Set.Nonempty U) : ∃ (K : TopologicalSpace.PositiveCompacts α), closure ↑K ⊆ U

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

Equations

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

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

• (_ : Nonempty (TopologicalSpace.PositiveCompacts α)) = (_ : Nonempty (TopologicalSpace.PositiveCompacts α))

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

• 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 : TopologicalSpace.PositiveCompacts α) (L : TopologicalSpace.PositiveCompacts β) : ↑(TopologicalSpace.PositiveCompacts.prod 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

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

Equations

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

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

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

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

@[simp]

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

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

Reinterpret a compact open as an open.

Equations

• TopologicalSpace.CompactOpens.toOpens s = { carrier := ↑s, is_open' := (_ : IsOpen ↑s) }

@[simp]

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

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

Reinterpret a compact open as a clopen.

Equations

• TopologicalSpace.CompactOpens.toClopens s = { carrier := ↑s, isClopen' := (_ : IsClosed ↑s ∧ IsOpen ↑s) }

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

@[simp]

theorem TopologicalSpace.CompactOpens.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : IsOpen s.carrier) : ↑{ toCompacts := s, isOpen' := h } = ↑s

instance TopologicalSpace.CompactOpens.instSupCompactOpens {α : Type u_1} [TopologicalSpace α] : Sup (TopologicalSpace.CompactOpens α)

Equations

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

instance TopologicalSpace.CompactOpens.instInfCompactOpens {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] : Inf (TopologicalSpace.CompactOpens α)

Equations

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

instance TopologicalSpace.CompactOpens.instSemilatticeInfCompactOpens {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] : SemilatticeInf (TopologicalSpace.CompactOpens α)

Equations

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

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

Equations

• TopologicalSpace.CompactOpens.instTopCompactOpens = { top := { toCompacts := ⊤, isOpen' := (_ : IsOpen Set.univ) } }

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

Equations

• TopologicalSpace.CompactOpens.instBotCompactOpens = { bot := { toCompacts := ⊥, isOpen' := (_ : IsOpen ∅) } }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

theorem TopologicalSpace.CompactOpens.coe_inf {α : Type u_1} [TopologicalSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) (t : TopologicalSpace.CompactOpens α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance TopologicalSpace.CompactOpens.instInhabitedCompactOpens {α : Type u_1} [TopologicalSpace α] : Inhabited (TopologicalSpace.CompactOpens α)

Equations

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

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

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' := (_ : IsOpen (f '' s.carrier)) }

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

@[simp]

theorem TopologicalSpace.CompactOpens.map_id {α : Type u_1} [TopologicalSpace α] (K : TopologicalSpace.CompactOpens α) : TopologicalSpace.CompactOpens.map id (_ : Continuous id) (_ : IsOpenMap 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 : TopologicalSpace.CompactOpens α) : TopologicalSpace.CompactOpens.map (f ∘ g) (_ : Continuous (f ∘ g)) (_ : IsOpenMap (f ∘ g)) K = TopologicalSpace.CompactOpens.map f hf hf' (TopologicalSpace.CompactOpens.map g hg hg' K)

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

• TopologicalSpace.CompactOpens.prod K L = let src := TopologicalSpace.Compacts.prod K.toCompacts L.toCompacts; { toCompacts := src, isOpen' := (_ : IsOpen (↑K ×ˢ ↑L.toCompacts)) }

@[simp]

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