topology.continuous_function.basic

structure continuous_map (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] :

Type (max u_1 u_2)

to_fun : α → β
continuous_to_fun : continuous self.to_fun . "continuity'"

The type of continuous maps from α to β.

When possible, instead of parametrizing results over (f : C(α, β)), you should parametrize over {F : Type*} [continuous_map_class F α β] (f : F).

When you extend this structure, make sure to extend continuous_map_class.

Instances for continuous_map

source

@[instance]

def continuous_map_class.to_fun_like (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [topological_space α] [topological_space β] [self : continuous_map_class F α β] :

fun_like F α (λ (_x : α), β)

source

@[class]

structure continuous_map_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [topological_space α] [topological_space β] :

Type (max u_1 u_2 u_3)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective continuous_map_class.coe
map_continuous : ∀ (f : F), continuous ⇑f

continuous_map_class F α β states that F is a type of continuous maps.

You should extend this class when you extend continuous_map.

Instances of this typeclass

Instances of other typeclasses for continuous_map_class

continuous_map_class.has_sizeof_inst

source

theorem map_continuous_at {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [continuous_map_class F α β] (f : F) (a : α) :

continuous_at ⇑f a

source

theorem map_continuous_within_at {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [continuous_map_class F α β] (f : F) (s : set α) (a : α) :

continuous_within_at ⇑f s a

source

@[protected, instance]

def continuous_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [continuous_map_class F α β] :

has_coe_t F C(α, β)

Equations

continuous_map.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, continuous_to_fun := _}}

source

@[protected, instance]

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

continuous_map_class C(α, β) α β

Equations

continuous_map.continuous_map_class = {coe := continuous_map.to_fun _inst_2, coe_injective' := _, map_continuous := _}

source

@[protected, instance]

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

has_coe_to_fun C(α, β) (λ (_x : C(α, β)), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

continuous_map.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem continuous_map.to_fun_eq_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : C(α, β)} :

f.to_fun = ⇑f

source

@[protected, simp, norm_cast]

theorem continuous_map.coe_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {F : Type u_3} [continuous_map_class F α β] (f : F) :

⇑↑f = ⇑f

source

@[ext]

theorem continuous_map.ext {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : C(α, β)} (h : ∀ (a : α), ⇑f a = ⇑g a) :

f = g

source

@[protected]

def continuous_map.copy {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (f' : α → β) (h : f' = ⇑f) :

C(α, β)

Copy of a continuous_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations

f.copy f' h = {to_fun := f', continuous_to_fun := _}

source

@[simp]

theorem continuous_map.coe_copy {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (f' : α → β) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

source

theorem continuous_map.copy_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (f' : α → β) (h : f' = ⇑f) :

f.copy f' h = f

source

@[protected]

theorem continuous_map.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) :

continuous ⇑f

Deprecated. Use map_continuous instead.

source

@[continuity]

theorem continuous_map.continuous_set_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set C(α, β)) (f : ↥s) :

continuous ⇑f

source

@[protected]

theorem continuous_map.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (x : α) :

continuous_at ⇑f x

Deprecated. Use map_continuous_at instead.

source

@[protected]

theorem continuous_map.congr_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : C(α, β)} (H : f = g) (x : α) :

⇑f x = ⇑g x

Deprecated. Use fun_like.congr_fun instead.

source

@[protected]

theorem continuous_map.congr_arg {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) {x y : α} (h : x = y) :

⇑f x = ⇑f y

Deprecated. Use fun_like.congr_arg instead.

source

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

function.injective coe_fn

source

@[simp]

theorem continuous_map.coe_mk {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (h : continuous f) :

⇑{to_fun := f, continuous_to_fun := h} = f

source

theorem continuous_map.map_specializes {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) {x y : α} (h : x ⤳ y) :

⇑f x ⤳ ⇑f y

source

def continuous_map.equiv_fn_of_discrete (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [discrete_topology α] :

C(α, β) ≃ (α → β)

The continuous functions from α to β are the same as the plain functions when α is discrete.

Equations

continuous_map.equiv_fn_of_discrete α β = {to_fun := λ (f : C(α, β)), ⇑f, inv_fun := λ (f : α → β), {to_fun := f, continuous_to_fun := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem continuous_map.equiv_fn_of_discrete_symm_apply_apply (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [discrete_topology α] (f : α → β) (ᾰ : α) :

⇑(⇑((continuous_map.equiv_fn_of_discrete α β).symm) f) ᾰ = f ᾰ

source

@[simp]

theorem continuous_map.equiv_fn_of_discrete_apply (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [discrete_topology α] (f : C(α, β)) (ᾰ : α) :

⇑(continuous_map.equiv_fn_of_discrete α β) f ᾰ = ⇑f ᾰ

source

@[protected]

def continuous_map.id (α : Type u_1) [topological_space α] :

C(α, α)

The identity as a continuous map.

Equations

continuous_map.id α = {to_fun := id α, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.coe_id (α : Type u_1) [topological_space α] :

⇑(continuous_map.id α) = id

source

def continuous_map.const (α : Type u_1) {β : Type u_2} [topological_space α] [topological_space β] (b : β) :

C(α, β)

The constant map as a continuous map.

Equations

continuous_map.const α b = {to_fun := function.const α b, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.coe_const (α : Type u_1) {β : Type u_2} [topological_space α] [topological_space β] (b : β) :

⇑(continuous_map.const α b) = function.const α b

source

@[protected, instance]

def continuous_map.inhabited (α : Type u_1) {β : Type u_2} [topological_space α] [topological_space β] [inhabited β] :

inhabited C(α, β)

Equations

continuous_map.inhabited α = {default := continuous_map.const α inhabited.default}

source

@[simp]

theorem continuous_map.id_apply {α : Type u_1} [topological_space α] (a : α) :

⇑(continuous_map.id α) a = a

source

@[simp]

theorem continuous_map.const_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (b : β) (a : α) :

⇑(continuous_map.const α b) a = b

source

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

C(α, γ)

The composition of continuous maps, as a continuous map.

Equations

f.comp g = {to_fun := ⇑f ∘ ⇑g, continuous_to_fun := _}

Instances for continuous_map.comp

nnreal.continuous_map.can_lift

source

@[simp]

theorem continuous_map.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(β, γ)) (g : C(α, β)) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem continuous_map.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(β, γ)) (g : C(α, β)) (a : α) :

⇑(f.comp g) a = ⇑f (⇑g a)

source

@[simp]

theorem continuous_map.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) :

(f.comp g).comp h = f.comp (g.comp h)

source

@[simp]

theorem continuous_map.id_comp {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) :

(continuous_map.id β).comp f = f

source

@[simp]

theorem continuous_map.comp_id {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) :

f.comp (continuous_map.id α) = f

source

@[simp]

theorem continuous_map.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (c : γ) (f : C(α, β)) :

(continuous_map.const β c).comp f = continuous_map.const α c

source

@[simp]

theorem continuous_map.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(β, γ)) (b : β) :

f.comp (continuous_map.const α b) = continuous_map.const α (⇑f b)

source

theorem continuous_map.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f₁ f₂ : C(β, γ)} {g : C(α, β)} (hg : function.surjective ⇑g) :

f₁.comp g = f₂.comp g ↔ f₁ = f₂

source

theorem continuous_map.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : function.injective ⇑f) :

f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

source

@[protected, instance]

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

nontrivial C(α, β)

source

def continuous_map.prod_mk {α : Type u_1} [topological_space α] {β₁ : Type u_7} {β₂ : Type u_8} [topological_space β₁] [topological_space β₂] (f : C(α, β₁)) (g : C(α, β₂)) :

C(α, β₁ × β₂)

Given two continuous maps f and g, this is the continuous map x ↦ (f x, g x).

Equations

f.prod_mk g = {to_fun := λ (x : α), (⇑f x, ⇑g x), continuous_to_fun := _}

source

def continuous_map.prod_map {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [topological_space α₁] [topological_space α₂] [topological_space β₁] [topological_space β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :

C(α₁ × β₁, α₂ × β₂)

Given two continuous maps f and g, this is the continuous map (x, y) ↦ (f x, g y).

Equations

f.prod_map g = {to_fun := prod.map ⇑f ⇑g, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.prod_map_apply {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [topological_space α₁] [topological_space α₂] [topological_space β₁] [topological_space β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) (x : α₁ × β₁) :

⇑(f.prod_map g) x = prod.map ⇑f ⇑g x

source

@[simp]

theorem continuous_map.prod_eval {α : Type u_1} [topological_space α] {β₁ : Type u_7} {β₂ : Type u_8} [topological_space β₁] [topological_space β₂] (f : C(α, β₁)) (g : C(α, β₂)) (a : α) :

⇑(f.prod_mk g) a = (⇑f a, ⇑g a)

source

def continuous_map.pi {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [topological_space A] [Π (i : I), topological_space (X i)] (f : Π (i : I), C(A, X i)) :

C(A, Π (i : I), X i)

Abbreviation for product of continuous maps, which is continuous

Equations

continuous_map.pi f = {to_fun := λ (a : A) (i : I), ⇑(f i) a, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.pi_eval {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [topological_space A] [Π (i : I), topological_space (X i)] (f : Π (i : I), C(A, X i)) (a : A) :

⇑(continuous_map.pi f) a = λ (i : I), ⇑(f i) a

source

def continuous_map.restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) (f : C(α, β)) :

C(↥s, β)

The restriction of a continuous function α → β to a subset s of α.

Equations

continuous_map.restrict s f = {to_fun := ⇑f ∘ coe, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.coe_restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) (f : C(α, β)) :

⇑(continuous_map.restrict s f) = ⇑f ∘ coe

source

@[simp]

theorem continuous_map.restrict_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set α) (x : ↥s) :

⇑(continuous_map.restrict s f) x = ⇑f ↑x

source

@[simp]

theorem continuous_map.restrict_apply_mk {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set α) (x : α) (hx : x ∈ s) :

⇑(continuous_map.restrict s f) ⟨x, hx⟩ = ⇑f x

source

@[simp]

theorem continuous_map.restrict_preimage_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set β) (ᾰ : ↥(⇑f ⁻¹' s)) :

⇑(f.restrict_preimage s) ᾰ = s.restrict_preimage ⇑f ᾰ

source

def continuous_map.restrict_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (s : set β) :

C(↥(⇑f ⁻¹' s), ↥s)

The restriction of a continuous map to the preimage of a set.

Equations

f.restrict_preimage s = {to_fun := s.restrict_preimage ⇑f, continuous_to_fun := _}

source

noncomputable def continuous_map.lift_cover {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {ι : Type u_5} (S : ι → set α) (φ : Π (i : ι), C(↥(S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), ⇑(φ i) ⟨x, hxi⟩ = ⇑(φ j) ⟨x, hxj⟩) (hS : ∀ (x : α), ∃ (i : ι), S i ∈ nhds x) :

C(α, β)

A family φ i of continuous maps C(S i, β), where the domains S i contain a neighbourhood of each point in α and the functions φ i agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

Equations

continuous_map.lift_cover S φ hφ hS = {to_fun := set.lift_cover S (λ (i : ι), ⇑(φ i)) hφ _, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.lift_cover_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {ι : Type u_5} {S : ι → set α} {φ : Π (i : ι), C(↥(S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), ⇑(φ i) ⟨x, hxi⟩ = ⇑(φ j) ⟨x, hxj⟩} {hS : ∀ (x : α), ∃ (i : ι), S i ∈ nhds x} {i : ι} (x : ↥(S i)) :

⇑(continuous_map.lift_cover S φ hφ hS) ↑x = ⇑(φ i) x

source

@[simp]

theorem continuous_map.lift_cover_restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {ι : Type u_5} {S : ι → set α} {φ : Π (i : ι), C(↥(S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), ⇑(φ i) ⟨x, hxi⟩ = ⇑(φ j) ⟨x, hxj⟩} {hS : ∀ (x : α), ∃ (i : ι), S i ∈ nhds x} {i : ι} :

continuous_map.restrict (S i) (continuous_map.lift_cover S φ hφ hS) = φ i

source

noncomputable def continuous_map.lift_cover' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (A : set (set α)) (F : Π (s : set α), s ∈ A → C(↥s, β)) (hF : ∀ (s : set α) (hs : s ∈ A) (t : set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t), ⇑(F s hs) ⟨x, hxi⟩ = ⇑(F t ht) ⟨x, hxj⟩) (hA : ∀ (x : α), ∃ (i : set α) (H : i ∈ A), i ∈ nhds x) :

C(α, β)

A family F s of continuous maps C(s, β), where (1) the domains s are taken from a set A of sets in α which contain a neighbourhood of each point in α and (2) the functions F s agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

Equations

continuous_map.lift_cover' A F hF hA = let S : ↥A → set α := coe, F_1 : Π (i : ↥A), C(↥i, β) := λ (i : ↥A), F ↑i _ in continuous_map.lift_cover S F_1 _ _

source

@[simp]

theorem continuous_map.lift_cover_coe' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {A : set (set α)} {F : Π (s : set α), s ∈ A → C(↥s, β)} {hF : ∀ (s : set α) (hs : s ∈ A) (t : set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t), ⇑(F s hs) ⟨x, hxi⟩ = ⇑(F t ht) ⟨x, hxj⟩} {hA : ∀ (x : α), ∃ (i : set α) (H : i ∈ A), i ∈ nhds x} {s : set α} {hs : s ∈ A} (x : ↥s) :

⇑(continuous_map.lift_cover' A F hF hA) ↑x = ⇑(F s hs) x

source

@[simp]

theorem continuous_map.lift_cover_restrict' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {A : set (set α)} {F : Π (s : set α), s ∈ A → C(↥s, β)} {hF : ∀ (s : set α) (hs : s ∈ A) (t : set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t), ⇑(F s hs) ⟨x, hxi⟩ = ⇑(F t ht) ⟨x, hxj⟩} {hA : ∀ (x : α), ∃ (i : set α) (H : i ∈ A), i ∈ nhds x} {s : set α} {hs : s ∈ A} :

continuous_map.restrict s (continuous_map.lift_cover' A F hF hA) = F s hs

source

@[simp]

theorem homeomorph.to_continuous_map_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) (ᾰ : α) :

⇑(e.to_continuous_map) ᾰ = ⇑e ᾰ

source

def homeomorph.to_continuous_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) :

C(α, β)

The forward direction of a homeomorphism, as a bundled continuous map.

Equations

e.to_continuous_map = {to_fun := ⇑e, continuous_to_fun := _}

source

@[protected, instance]

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

has_coe (α ≃ₜ β) C(α, β)

homeomorph.to_continuous_map as a coercion.

Equations

homeomorph.continuous_map.has_coe = {coe := homeomorph.to_continuous_map _inst_2}

source

theorem homeomorph.to_continuous_map_as_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :

f.to_continuous_map = ↑f

source

@[simp]

theorem homeomorph.coe_refl {α : Type u_1} [topological_space α] :

↑(homeomorph.refl α) = continuous_map.id α

source

@[simp]

theorem homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) :

↑(f.trans g) = ↑g.comp ↑f

source

@[simp]

theorem homeomorph.symm_comp_to_continuous_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :

↑(f.symm).comp ↑f = continuous_map.id α

Left inverse to a continuous map from a homeomorphism, mirroring equiv.symm_comp_self.

source

@[simp]

theorem homeomorph.to_continuous_map_comp_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :

↑f.comp ↑(f.symm) = continuous_map.id β

Right inverse to a continuous map from a homeomorphism, mirroring equiv.self_comp_symm.

mathlib3 documentation

Continuous bundled maps #

Continuous maps #