mathlib documentation

topology.compact_open

def continuous_map.compact_open.gen {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) (u : set β) :

Equations

continuous_map.compact_open.gen s u = {f : C(α, β) | ⇑f '' s ⊆ u}

@[instance]

def continuous_map.compact_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

topological_space C(α, β)

Equations

continuous_map.compact_open = topological_space.generate_from {m : set C(α, β) | ∃ (s : set α) (hs : is_compact s) (u : set β) (hu : is_open u), m = continuous_map.compact_open.gen s u}

def continuous_map.induced {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} (hg : continuous g) (f : C(α, β)) :

C(α, γ)

Equations

continuous_map.induced hg f = {to_fun := g ∘ ⇑f, continuous_to_fun := _}

theorem continuous_map.continuous_induced {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} (hg : continuous g) :

continuous (continuous_map.induced hg)

C(α, -) is a functor.

def continuous_map.ev (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] (p : C(α, β) × α) :

β

Equations

continuous_map.ev α β p = ⇑(p.fst) p.snd

theorem continuous_map.continuous_ev {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [locally_compact_space α] :

continuous (continuous_map.ev α β)

def continuous_map.coev (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] (b : β) :

C(α, β × α)

Equations

continuous_map.coev α β b = {to_fun := λ (a : α), (b, a), continuous_to_fun := _}

theorem continuous_map.image_coev {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {y : β} (s : set α) :

⇑(continuous_map.coev α β y) '' s = {y}.prod s

theorem continuous_map.continuous_coev {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

continuous (continuous_map.coev α β)