mathlib documentation

topology.compact_open

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

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

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

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

C(α, -) is a functor.

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

Equations
def continuous_map.coev (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] :
β → C(α, β × α)

Equations
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 β] :