def
continuous_map.compact_open.gen
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
@[instance]
def
continuous_map.compact_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
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 : β → γ} :
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) :
C(α, -) is a functor.
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 β] :
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 β] :