Compact sets #

The type of non-empty compact subsets of a topological space. The non-emptiness will be useful in metric spaces, as we will be able to put a distance (and not merely an edistance) on this space.

Equations

topological_space.nonempty_compacts α = {s // s.nonempty ∧ is_compact s}

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

topological_space.nonempty_compacts_inhabited α = {default := ⟨{default α}, _⟩}

source

@[nolint]

def topological_space.positive_compacts (α : Type u_1) [topological_space α] :

Type u_1

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

Equations

topological_space.positive_compacts α = {s // is_compact s ∧ (interior s).nonempty}

source

@[protected, instance]

def topological_space.compacts.semilattice_sup_bot {α : Type u_1} [topological_space α] :

semilattice_sup_bot (topological_space.compacts α)

Equations

topological_space.compacts.semilattice_sup_bot = subtype.semilattice_sup_bot compact_empty topological_space.compacts.semilattice_sup_bot._proof_1

source

@[protected, instance]

def topological_space.compacts.semilattice_inf_bot {α : Type u_1} [topological_space α] [t2_space α] :

semilattice_inf_bot (topological_space.compacts α)

Equations

topological_space.compacts.semilattice_inf_bot = subtype.semilattice_inf_bot compact_empty topological_space.compacts.semilattice_inf_bot._proof_1

source

@[protected, instance]

def topological_space.compacts.lattice {α : Type u_1} [topological_space α] [t2_space α] :

lattice (topological_space.compacts α)

Equations

topological_space.compacts.lattice = subtype.lattice topological_space.compacts.lattice._proof_1 topological_space.compacts.lattice._proof_2

source

@[simp]

theorem topological_space.compacts.bot_val {α : Type u_1} [topological_space α] :

⊥.val = ∅

source

@[simp]

theorem topological_space.compacts.sup_val {α : Type u_1} [topological_space α] {K₁ K₂ : topological_space.compacts α} :

(K₁ ⊔ K₂).val = K₁.val ∪ K₂.val

source

@[protected, ext]

theorem topological_space.compacts.ext {α : Type u_1} [topological_space α] {K₁ K₂ : topological_space.compacts α} (h : K₁.val = K₂.val) :

K₁ = K₂

source

@[simp]

theorem topological_space.compacts.finset_sup_val {α : Type u_1} [topological_space α] {β : Type u_2} {K : β → topological_space.compacts α} {s : finset β} :

(s.sup K).val = s.sup (λ (x : β), (K x).val)

source

@[protected, instance]

def topological_space.compacts.inhabited {α : Type u_1} [topological_space α] :

inhabited (topological_space.compacts α)

Equations

topological_space.compacts.inhabited = {default := ⊥}

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

topological_space.compacts.map f hf K = ⟨f '' K.val, _⟩

source

@[simp]

theorem topological_space.compacts.map_val {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (K : topological_space.compacts α) :

(topological_space.compacts.map f hf K).val = f '' K.val

source

@[protected, simp]

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

topological_space.compacts.equiv f = {to_fun := topological_space.compacts.map ⇑f _, inv_fun := topological_space.compacts.map ⇑(f.symm) _, left_inv := _, right_inv := _}

source

theorem topological_space.compacts.equiv_to_fun_val {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) (K : topological_space.compacts α) :

(⇑(topological_space.compacts.equiv f) K).val = ⇑(f.symm) ⁻¹' K.val

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

source

@[protected, instance]

def topological_space.nonempty_compacts.to_compact_space {α : Type u_1} [topological_space α] {p : topological_space.nonempty_compacts α} :

compact_space ↥(p.val)

source

@[protected, instance]

def topological_space.nonempty_compacts.to_nonempty {α : Type u_1} [topological_space α] {p : topological_space.nonempty_compacts α} :

nonempty ↥(p.val)

source

def topological_space.nonempty_compacts.to_closeds {α : Type u_1} [topological_space α] [t2_space α] :

topological_space.nonempty_compacts α → topological_space.closeds α

Associate to a nonempty compact subset the corresponding closed subset

Equations

topological_space.nonempty_compacts.to_closeds = set.inclusion topological_space.nonempty_compacts.to_closeds._proof_1