mathlib3 documentation

topology.sets.compacts

Compact sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main Definitions #

For a topological space α,

Compact sets #

source
structure topological_space.compacts (α : Type u_4) [topological_space α] :
Type u_4

The type of compact sets of a topological space.

Instances for topological_space.compacts
source
@[protected, instance]
def topological_space.compacts.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.compacts α) α
Equations
source
@[protected]
theorem topological_space.compacts.is_compact {α : Type u_1} [topological_space α] (s : topological_space.compacts α) :
is_compact ↑s
source
@[protected, instance]
def topological_space.compacts.compact_space {α : Type u_1} [topological_space α] (K : topological_space.compacts α) :
compact_space ↥K
source
@[protected, instance]
def topological_space.compacts.is_compact.can_lift {α : Type u_1} [topological_space α] :
can_lift (set α) (topological_space.compacts α) coe is_compact
Equations
source
@[protected, ext]
theorem topological_space.compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.compacts α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.compacts.coe_mk {α : Type u_1} [topological_space α] (s : set α) (h : is_compact s) :
↑{carrier := s, is_compact' := h} = s
source
@[simp]
theorem topological_space.compacts.carrier_eq_coe {α : Type u_1} [topological_space α] (s : topological_space.compacts α) :
s.carrier = ↑s
source
@[protected, instance]
def topological_space.compacts.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.has_inf {α : Type u_1} [topological_space α] [t2_space α] :
has_inf (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.has_top {α : Type u_1} [topological_space α] [compact_space α] :
has_top (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.has_bot {α : Type u_1} [topological_space α] :
has_bot (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.distrib_lattice {α : Type u_1} [topological_space α] [t2_space α] :
distrib_lattice (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.order_bot {α : Type u_1} [topological_space α] :
order_bot (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.bounded_order {α : Type u_1} [topological_space α] [compact_space α] :
bounded_order (topological_space.compacts α)
Equations
source
@[protected, instance]
def topological_space.compacts.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.compacts α)

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

Equations
source
@[simp]
theorem topological_space.compacts.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.compacts α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.compacts.coe_inf {α : Type u_1} [topological_space α] [t2_space α] (s t : topological_space.compacts α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem topological_space.compacts.coe_top {α : Type u_1} [topological_space α] [compact_space α] :
↑⊤ = set.univ
source
@[simp]
theorem topological_space.compacts.coe_bot {α : Type u_1} [topological_space α] :
↑⊥ = ∅
source
@[simp]
theorem topological_space.compacts.coe_finset_sup {α : Type u_1} [topological_space α] {ι : Type u_2} {s : finset ι} {f : ι → topological_space.compacts α} :
↑(s.sup f) = s.sup (λ (i : ι), ↑(f i))
source
@[protected]
def topological_space.compacts.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (K : topological_space.compacts α) :
topological_space.compacts β

The image of a compact set under a continuous function.

Equations
source
@[simp, norm_cast]
theorem topological_space.compacts.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (s : topological_space.compacts α) :
↑(topological_space.compacts.map f hf s) = f '' ↑s
source
@[simp]
theorem topological_space.compacts.map_id {α : Type u_1} [topological_space α] (K : topological_space.compacts α) :
topological_space.compacts.map id continuous_id K = K
source
theorem topological_space.compacts.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g) (K : topological_space.compacts α) :
topological_space.compacts.map (f ∘ g) _ K = topological_space.compacts.map f hf (topological_space.compacts.map g hg K)
source
@[simp]
theorem topological_space.compacts.equiv_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) (K : topological_space.compacts α) :
⇑(topological_space.compacts.equiv f) K = topological_space.compacts.map ⇑f _ K
source
@[protected]
def topological_space.compacts.equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
topological_space.compacts α ≃ topological_space.compacts β

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

Equations
source
@[simp]
theorem topological_space.compacts.equiv_symm_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) (K : topological_space.compacts β) :
⇑((topological_space.compacts.equiv f).symm) K = topological_space.compacts.map ⇑(f.symm) _ K
source
@[simp]
theorem topological_space.compacts.equiv_refl {α : Type u_1} [topological_space α] :
topological_space.compacts.equiv (homeomorph.refl α) = equiv.refl (topological_space.compacts α)
source
@[simp]
theorem topological_space.compacts.equiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
topological_space.compacts.equiv (f.trans g) = (topological_space.compacts.equiv f).trans (topological_space.compacts.equiv g)
source
@[simp]
theorem topological_space.compacts.equiv_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
topological_space.compacts.equiv f.symm = (topological_space.compacts.equiv f).symm
source
theorem topological_space.compacts.coe_equiv_apply_eq_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) (K : topological_space.compacts α) :
↑(⇑(topological_space.compacts.equiv f) K) = ⇑(f.symm) ⁻¹' ↑K

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

source
@[protected]
def topological_space.compacts.prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.compacts α) (L : topological_space.compacts β) :
topological_space.compacts (α × β)

The product of two compacts, as a compacts in the product space.

Equations
source
@[simp]
theorem topological_space.compacts.coe_prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.compacts α) (L : topological_space.compacts β) :
↑(K.prod L) = ↑K ×ˢ ↑L

Nonempty compact sets #

source
structure topological_space.nonempty_compacts (α : Type u_4) [topological_space α] :
Type u_4

The type of nonempty compact sets of a topological space.

Instances for topological_space.nonempty_compacts
source
@[protected, instance]
def topological_space.nonempty_compacts.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.nonempty_compacts α) α
Equations
source
@[protected]
theorem topological_space.nonempty_compacts.is_compact {α : Type u_1} [topological_space α] (s : topological_space.nonempty_compacts α) :
is_compact ↑s
source
@[protected]
theorem topological_space.nonempty_compacts.nonempty {α : Type u_1} [topological_space α] (s : topological_space.nonempty_compacts α) :
↑s.nonempty
source
def topological_space.nonempty_compacts.to_closeds {α : Type u_1} [topological_space α] [t2_space α] (s : topological_space.nonempty_compacts α) :
topological_space.closeds α

Reinterpret a nonempty compact as a closed set.

Equations
source
@[protected, ext]
theorem topological_space.nonempty_compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.nonempty_compacts α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.nonempty_compacts.coe_mk {α : Type u_1} [topological_space α] (s : topological_space.compacts α) (h : s.carrier.nonempty) :
↑{to_compacts := s, nonempty' := h} = ↑s
source
@[simp]
theorem topological_space.nonempty_compacts.carrier_eq_coe {α : Type u_1} [topological_space α] (s : topological_space.nonempty_compacts α) :
s.to_compacts.carrier = ↑s
source
@[protected, instance]
def topological_space.nonempty_compacts.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.nonempty_compacts α)
Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.has_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
has_top (topological_space.nonempty_compacts α)
Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.nonempty_compacts α)
Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.order_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
order_top (topological_space.nonempty_compacts α)
Equations
source
@[simp]
theorem topological_space.nonempty_compacts.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.nonempty_compacts α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.nonempty_compacts.coe_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
↑⊤ = set.univ
source
@[protected, instance]
def topological_space.nonempty_compacts.inhabited {α : Type u_1} [topological_space α] [inhabited α] :
inhabited (topological_space.nonempty_compacts α)

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

Equations
source
@[protected, instance]
def topological_space.nonempty_compacts.to_compact_space {α : Type u_1} [topological_space α] {s : topological_space.nonempty_compacts α} :
compact_space ↥s
source
@[protected, instance]
def topological_space.nonempty_compacts.to_nonempty {α : Type u_1} [topological_space α] {s : topological_space.nonempty_compacts α} :
nonempty ↥s
source
@[protected]
def topological_space.nonempty_compacts.prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.nonempty_compacts α) (L : topological_space.nonempty_compacts β) :
topological_space.nonempty_compacts (α × β)

The product of two nonempty_compacts, as a nonempty_compacts in the product space.

Equations
source
@[simp]
theorem topological_space.nonempty_compacts.coe_prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.nonempty_compacts α) (L : topological_space.nonempty_compacts β) :
↑(K.prod L) = ↑K ×ˢ ↑L

Positive compact sets #

source
structure topological_space.positive_compacts (α : Type u_4) [topological_space α] :
Type u_4

The type of compact sets with nonempty interior of a topological space. See also compacts and nonempty_compacts.

Instances for topological_space.positive_compacts
source
@[protected, instance]
def topological_space.positive_compacts.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.positive_compacts α) α
Equations
source
@[protected]
theorem topological_space.positive_compacts.is_compact {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
is_compact ↑s
source
theorem topological_space.positive_compacts.interior_nonempty {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
(interior ↑s).nonempty
source
@[protected]
theorem topological_space.positive_compacts.nonempty {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
↑s.nonempty
source
def topological_space.positive_compacts.to_nonempty_compacts {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
topological_space.nonempty_compacts α

Reinterpret a positive compact as a nonempty compact.

Equations
source
@[protected, ext]
theorem topological_space.positive_compacts.ext {α : Type u_1} [topological_space α] {s t : topological_space.positive_compacts α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.positive_compacts.coe_mk {α : Type u_1} [topological_space α] (s : topological_space.compacts α) (h : (interior s.carrier).nonempty) :
↑{to_compacts := s, interior_nonempty' := h} = ↑s
source
@[simp]
theorem topological_space.positive_compacts.carrier_eq_coe {α : Type u_1} [topological_space α] (s : topological_space.positive_compacts α) :
s.to_compacts.carrier = ↑s
source
@[protected, instance]
def topological_space.positive_compacts.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.has_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
has_top (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.order_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
order_top (topological_space.positive_compacts α)
Equations
source
@[simp]
theorem topological_space.positive_compacts.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.positive_compacts α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.positive_compacts.coe_top {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
↑⊤ = set.univ
source
@[protected]
def topological_space.positive_compacts.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (hf' : is_open_map f) (K : topological_space.positive_compacts α) :
topological_space.positive_compacts β

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

Equations
source
@[simp, norm_cast]
theorem topological_space.positive_compacts.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : topological_space.positive_compacts α) :
↑(topological_space.positive_compacts.map f hf hf' s) = f '' ↑s
source
@[simp]
theorem topological_space.positive_compacts.map_id {α : Type u_1} [topological_space α] (K : topological_space.positive_compacts α) :
topological_space.positive_compacts.map id continuous_id is_open_map.id K = K
source
theorem topological_space.positive_compacts.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g) (hf' : is_open_map f) (hg' : is_open_map g) (K : topological_space.positive_compacts α) :
topological_space.positive_compacts.map (f ∘ g) _ _ K = topological_space.positive_compacts.map f hf hf' (topological_space.positive_compacts.map g hg hg' K)
source
theorem exists_positive_compacts_subset {α : Type u_1} [topological_space α] [locally_compact_space α] {U : set α} (ho : is_open U) (hn : U.nonempty) :
∃ (K : topological_space.positive_compacts α), ↑K ⊆ U
source
@[protected, instance]
def topological_space.positive_compacts.inhabited {α : Type u_1} [topological_space α] [compact_space α] [nonempty α] :
inhabited (topological_space.positive_compacts α)
Equations
source
@[protected, instance]
def topological_space.positive_compacts.nonempty' {α : Type u_1} [topological_space α] [locally_compact_space α] [nonempty α] :
nonempty (topological_space.positive_compacts α)

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

source
@[protected]
def topological_space.positive_compacts.prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.positive_compacts α) (L : topological_space.positive_compacts β) :
topological_space.positive_compacts (α × β)

The product of two positive_compacts, as a positive_compacts in the product space.

Equations
source
@[simp]
theorem topological_space.positive_compacts.coe_prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.positive_compacts α) (L : topological_space.positive_compacts β) :
↑(K.prod L) = ↑K ×ˢ ↑L

Compact open sets #

source
structure topological_space.compact_opens (α : Type u_4) [topological_space α] :
Type u_4

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

Instances for topological_space.compact_opens
source
@[protected, instance]
def topological_space.compact_opens.set_like {α : Type u_1} [topological_space α] :
set_like (topological_space.compact_opens α) α
Equations
source
@[protected]
theorem topological_space.compact_opens.is_compact {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
is_compact ↑s
source
@[protected]
theorem topological_space.compact_opens.is_open {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
is_open ↑s
source
def topological_space.compact_opens.to_opens {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
topological_space.opens α

Reinterpret a compact open as an open.

Equations
source
@[simp]
theorem topological_space.compact_opens.to_opens_coe {α : Type u_1} [topological_space α] (s : topological_space.compact_opens α) :
↑(s.to_opens) = ↑s
source
@[simp]
theorem topological_space.compact_opens.to_clopens_carrier {α : Type u_1} [topological_space α] [t2_space α] (s : topological_space.compact_opens α) :
s.to_clopens.carrier = ↑s
source
def topological_space.compact_opens.to_clopens {α : Type u_1} [topological_space α] [t2_space α] (s : topological_space.compact_opens α) :
topological_space.clopens α

Reinterpret a compact open as a clopen.

Equations
source
@[protected, ext]
theorem topological_space.compact_opens.ext {α : Type u_1} [topological_space α] {s t : topological_space.compact_opens α} (h : ↑s = ↑t) :
s = t
source
@[simp]
theorem topological_space.compact_opens.coe_mk {α : Type u_1} [topological_space α] (s : topological_space.compacts α) (h : is_open s.carrier) :
↑{to_compacts := s, is_open' := h} = ↑s
source
@[protected, instance]
def topological_space.compact_opens.has_sup {α : Type u_1} [topological_space α] :
has_sup (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_inf {α : Type u_1} [topological_space α] [quasi_separated_space α] :
has_inf (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.semilattice_inf {α : Type u_1} [topological_space α] [quasi_separated_space α] :
semilattice_inf (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_top {α : Type u_1} [topological_space α] [compact_space α] :
has_top (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_bot {α : Type u_1} [topological_space α] :
has_bot (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_sdiff {α : Type u_1} [topological_space α] [t2_space α] :
has_sdiff (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.has_compl {α : Type u_1} [topological_space α] [t2_space α] [compact_space α] :
has_compl (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.semilattice_sup {α : Type u_1} [topological_space α] :
semilattice_sup (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.order_bot {α : Type u_1} [topological_space α] :
order_bot (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.generalized_boolean_algebra {α : Type u_1} [topological_space α] [t2_space α] :
generalized_boolean_algebra (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.bounded_order {α : Type u_1} [topological_space α] [compact_space α] :
bounded_order (topological_space.compact_opens α)
Equations
source
@[protected, instance]
def topological_space.compact_opens.boolean_algebra {α : Type u_1} [topological_space α] [t2_space α] [compact_space α] :
boolean_algebra (topological_space.compact_opens α)
Equations
  • topological_space.compact_opens.boolean_algebra = function.injective.boolean_algebra coe topological_space.compact_opens.boolean_algebra._proof_1 topological_space.compact_opens.boolean_algebra._proof_2 topological_space.compact_opens.boolean_algebra._proof_3 topological_space.compact_opens.boolean_algebra._proof_4 topological_space.compact_opens.boolean_algebra._proof_5 topological_space.compact_opens.boolean_algebra._proof_6 topological_space.compact_opens.boolean_algebra._proof_7
source
@[simp]
theorem topological_space.compact_opens.coe_sup {α : Type u_1} [topological_space α] (s t : topological_space.compact_opens α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem topological_space.compact_opens.coe_inf {α : Type u_1} [topological_space α] [t2_space α] (s t : topological_space.compact_opens α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem topological_space.compact_opens.coe_top {α : Type u_1} [topological_space α] [compact_space α] :
↑⊤ = set.univ
source
@[simp]
theorem topological_space.compact_opens.coe_bot {α : Type u_1} [topological_space α] :
↑⊥ = ∅
source
@[simp]
theorem topological_space.compact_opens.coe_sdiff {α : Type u_1} [topological_space α] [t2_space α] (s t : topological_space.compact_opens α) :
↑(s \ t) = ↑s \ ↑t
source
@[simp]
theorem topological_space.compact_opens.coe_compl {α : Type u_1} [topological_space α] [t2_space α] [compact_space α] (s : topological_space.compact_opens α) :
↑sᶜ = (↑s)ᶜ
source
@[protected, instance]
def topological_space.compact_opens.inhabited {α : Type u_1} [topological_space α] :
inhabited (topological_space.compact_opens α)
Equations
source
def topological_space.compact_opens.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
topological_space.compact_opens β

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

Equations
source
@[simp]
theorem topological_space.compact_opens.map_to_compacts {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
(topological_space.compact_opens.map f hf hf' s).to_compacts = topological_space.compacts.map f hf s.to_compacts
source
@[simp, norm_cast]
theorem topological_space.compact_opens.coe_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : topological_space.compact_opens α) :
↑(topological_space.compact_opens.map f hf hf' s) = f '' ↑s
source
@[simp]
theorem topological_space.compact_opens.map_id {α : Type u_1} [topological_space α] (K : topological_space.compact_opens α) :
topological_space.compact_opens.map id continuous_id is_open_map.id K = K
source
theorem topological_space.compact_opens.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g) (hf' : is_open_map f) (hg' : is_open_map g) (K : topological_space.compact_opens α) :
topological_space.compact_opens.map (f ∘ g) _ _ K = topological_space.compact_opens.map f hf hf' (topological_space.compact_opens.map g hg hg' K)
source
@[protected]
def topological_space.compact_opens.prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.compact_opens α) (L : topological_space.compact_opens β) :
topological_space.compact_opens (α × β)

The product of two compact_opens, as a compact_opens in the product space.

Equations
source
@[simp]
theorem topological_space.compact_opens.coe_prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (K : topological_space.compact_opens α) (L : topological_space.compact_opens β) :
↑(K.prod L) = ↑K ×ˢ ↑L