Continuous functions vanishing at infinity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The type of continuous functions vanishing at infinity. When the domain is compact
C(α, β) ≃ C₀(α, β) via the identity map. When the codomain is a metric space, every continuous
map which vanishes at infinity is a bounded continuous function. When the domain is a locally
compact space, this type has nice properties.
TODO #
- Create more intances of algebraic structures (e.g.,
non_unital_semiring) once the necessary type classes (e.g.,topological_ring) are sufficiently generalized. - Relate the unitization of
C₀(α, β)to the Alexandroff compactification.
structure
zero_at_infty_continuous_map
(α : Type u)
(β : Type v)
[topological_space α]
[has_zero β]
[topological_space β] :
Type (max u v)
- to_continuous_map : C(α, β)
- zero_at_infty' : filter.tendsto self.to_continuous_map.to_fun (filter.cocompact α) (nhds 0)
C₀(α, β) is the type of continuous functions α → β which vanish at infinity from a
topological space to a metric space with a zero element.
When possible, instead of parametrizing results over (f : C₀(α, β)),
you should parametrize over (F : Type*) [zero_at_infty_continuous_map_class F α β] (f : F).
When you extend this structure, make sure to extend zero_at_infty_continuous_map_class.
Instances for zero_at_infty_continuous_map
- zero_at_infty_continuous_map.has_sizeof_inst
- zero_at_infty_continuous_map.zero_at_infty_continuous_map_class
- zero_at_infty_continuous_map.has_coe_to_fun
- zero_at_infty_continuous_map.has_coe_t
- zero_at_infty_continuous_map.has_zero
- zero_at_infty_continuous_map.inhabited
- zero_at_infty_continuous_map.has_mul
- zero_at_infty_continuous_map.mul_zero_class
- zero_at_infty_continuous_map.semigroup_with_zero
- zero_at_infty_continuous_map.has_add
- zero_at_infty_continuous_map.add_zero_class
- zero_at_infty_continuous_map.has_nat_scalar
- zero_at_infty_continuous_map.add_monoid
- zero_at_infty_continuous_map.add_comm_monoid
- zero_at_infty_continuous_map.has_neg
- zero_at_infty_continuous_map.has_sub
- zero_at_infty_continuous_map.has_int_scalar
- zero_at_infty_continuous_map.add_group
- zero_at_infty_continuous_map.add_comm_group
- zero_at_infty_continuous_map.has_smul
- zero_at_infty_continuous_map.is_central_scalar
- zero_at_infty_continuous_map.smul_with_zero
- zero_at_infty_continuous_map.mul_action_with_zero
- zero_at_infty_continuous_map.module
- zero_at_infty_continuous_map.non_unital_non_assoc_semiring
- zero_at_infty_continuous_map.non_unital_semiring
- zero_at_infty_continuous_map.non_unital_comm_semiring
- zero_at_infty_continuous_map.non_unital_non_assoc_ring
- zero_at_infty_continuous_map.non_unital_ring
- zero_at_infty_continuous_map.non_unital_comm_ring
- zero_at_infty_continuous_map.is_scalar_tower
- zero_at_infty_continuous_map.smul_comm_class
- zero_at_infty_continuous_map.metric_space
- zero_at_infty_continuous_map.complete_space
- zero_at_infty_continuous_map.normed_add_comm_group
- zero_at_infty_continuous_map.normed_space
- zero_at_infty_continuous_map.non_unital_normed_ring
- zero_at_infty_continuous_map.has_star
- zero_at_infty_continuous_map.star_add_monoid
- zero_at_infty_continuous_map.normed_star_group
- zero_at_infty_continuous_map.star_module
- zero_at_infty_continuous_map.star_ring
- zero_at_infty_continuous_map.cstar_ring
@[class]
structure
zero_at_infty_continuous_map_class
(F : Type u_2)
(α : out_param (Type u_3))
(β : out_param (Type u_4))
[topological_space α]
[has_zero β]
[topological_space β] :
Type (max u_2 u_3 u_4)
- coe : F → Π (a : α), (λ (_x : α), β) a
- coe_injective' : function.injective zero_at_infty_continuous_map_class.coe
- map_continuous : ∀ (f : F), continuous ⇑f
- zero_at_infty : ∀ (f : F), filter.tendsto ⇑f (filter.cocompact α) (nhds 0)
zero_at_infty_continuous_map_class F α β states that F is a type of continuous maps which
vanish at infinity.
You should also extend this typeclass when you extend zero_at_infty_continuous_map.
Instances of this typeclass
Instances of other typeclasses for zero_at_infty_continuous_map_class
- zero_at_infty_continuous_map_class.has_sizeof_inst
@[instance]
def
zero_at_infty_continuous_map_class.to_continuous_map_class
(F : Type u_2)
(α : out_param (Type u_3))
(β : out_param (Type u_4))
[topological_space α]
[has_zero β]
[topological_space β]
[self : zero_at_infty_continuous_map_class F α β] :
continuous_map_class F α β
@[protected, instance]
def
zero_at_infty_continuous_map.zero_at_infty_continuous_map_class
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β] :
Equations
- zero_at_infty_continuous_map.zero_at_infty_continuous_map_class = {coe := λ (f : zero_at_infty_continuous_map α β), f.to_continuous_map.to_fun, coe_injective' := _, map_continuous := _, zero_at_infty := _}
@[protected, instance]
def
zero_at_infty_continuous_map.has_coe_to_fun
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β] :
has_coe_to_fun (zero_at_infty_continuous_map α β) (λ (_x : zero_at_infty_continuous_map α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[protected, instance]
def
zero_at_infty_continuous_map.has_coe_t
{F : Type u_1}
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
[zero_at_infty_continuous_map_class F α β] :
Equations
- zero_at_infty_continuous_map.has_coe_t = {coe := λ (f : F), {to_continuous_map := {to_fun := ⇑f, continuous_to_fun := _}, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_to_continuous_fun
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β) :
⇑(f.to_continuous_map) = ⇑f
@[ext]
theorem
zero_at_infty_continuous_map.ext
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{f g : zero_at_infty_continuous_map α β}
(h : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
@[protected]
def
zero_at_infty_continuous_map.copy
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β)
(f' : α → β)
(h : f' = ⇑f) :
Copy of a zero_at_infinity_continuous_map with a new to_fun equal to the old one. Useful
to fix definitional equalities.
Equations
- f.copy f' h = {to_continuous_map := {to_fun := f', continuous_to_fun := _}, zero_at_infty' := _}
@[simp]
theorem
zero_at_infty_continuous_map.coe_copy
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β)
(f' : α → β)
(h : f' = ⇑f) :
theorem
zero_at_infty_continuous_map.copy_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β)
(f' : α → β)
(h : f' = ⇑f) :
theorem
zero_at_infty_continuous_map.eq_of_empty
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
[is_empty α]
(f g : zero_at_infty_continuous_map α β) :
f = g
def
zero_at_infty_continuous_map.continuous_map.lift_zero_at_infty
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
[compact_space α] :
C(α, β) ≃ zero_at_infty_continuous_map α β
A continuous function on a compact space is automatically a continuous function vanishing at infinity.
Equations
- zero_at_infty_continuous_map.continuous_map.lift_zero_at_infty = {to_fun := λ (f : C(α, β)), {to_continuous_map := {to_fun := ⇑f, continuous_to_fun := _}, zero_at_infty' := _}, inv_fun := λ (f : zero_at_infty_continuous_map α β), ↑f, left_inv := _, right_inv := _}
@[simp]
theorem
zero_at_infty_continuous_map.continuous_map.lift_zero_at_infty_apply_to_continuous_map_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
[compact_space α]
(f : C(α, β))
(ᾰ : α) :
@[simp]
theorem
zero_at_infty_continuous_map.continuous_map.lift_zero_at_infty_symm_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
[compact_space α]
(f : zero_at_infty_continuous_map α β) :
def
zero_at_infty_continuous_map.zero_at_infty_continuous_map_class.of_compact
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{G : Type u_1}
[continuous_map_class G α β]
[compact_space α] :
A continuous function on a compact space is automatically a continuous function vanishing at infinity. This is not an instance to avoid type class loops.
Equations
- zero_at_infty_continuous_map.zero_at_infty_continuous_map_class.of_compact = {coe := λ (g : G), ⇑g, coe_injective' := _, map_continuous := _, zero_at_infty := _}
@[simp]
theorem
zero_at_infty_continuous_map.zero_at_infty_continuous_map_class.of_compact_coe
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{G : Type u_1}
[continuous_map_class G α β]
[compact_space α]
(g : G)
(a : α) :
Algebraic structure #
Whenever β has suitable algebraic structure and a compatible topological structure, then
C₀(α, β) inherits a corresponding algebraic structure. The primary exception to this is that
C₀(α, β) will not have a multiplicative identity.
@[protected, instance]
def
zero_at_infty_continuous_map.has_zero
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β] :
Equations
- zero_at_infty_continuous_map.has_zero = {zero := {to_continuous_map := 0, zero_at_infty' := _}}
@[protected, instance]
def
zero_at_infty_continuous_map.inhabited
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β] :
Equations
@[simp]
theorem
zero_at_infty_continuous_map.coe_zero
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β] :
theorem
zero_at_infty_continuous_map.zero_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α)
[has_zero β] :
@[protected, instance]
def
zero_at_infty_continuous_map.has_mul
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[mul_zero_class β]
[has_continuous_mul β] :
Equations
- zero_at_infty_continuous_map.has_mul = {mul := λ (f g : zero_at_infty_continuous_map α β), {to_continuous_map := ↑f * ↑g, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_mul
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[mul_zero_class β]
[has_continuous_mul β]
(f g : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.mul_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α)
[mul_zero_class β]
[has_continuous_mul β]
(f g : zero_at_infty_continuous_map α β) :
@[protected, instance]
def
zero_at_infty_continuous_map.mul_zero_class
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[mul_zero_class β]
[has_continuous_mul β] :
Equations
- zero_at_infty_continuous_map.mul_zero_class = function.injective.mul_zero_class coe_fn zero_at_infty_continuous_map.mul_zero_class._proof_1 zero_at_infty_continuous_map.mul_zero_class._proof_2 zero_at_infty_continuous_map.coe_mul
@[protected, instance]
def
zero_at_infty_continuous_map.semigroup_with_zero
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[semigroup_with_zero β]
[has_continuous_mul β] :
Equations
- zero_at_infty_continuous_map.semigroup_with_zero = function.injective.semigroup_with_zero coe_fn zero_at_infty_continuous_map.semigroup_with_zero._proof_1 zero_at_infty_continuous_map.semigroup_with_zero._proof_2 zero_at_infty_continuous_map.semigroup_with_zero._proof_3
@[protected, instance]
def
zero_at_infty_continuous_map.has_add
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_zero_class β]
[has_continuous_add β] :
Equations
- zero_at_infty_continuous_map.has_add = {add := λ (f g : zero_at_infty_continuous_map α β), {to_continuous_map := ↑f + ↑g, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_add
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_zero_class β]
[has_continuous_add β]
(f g : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.add_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α)
[add_zero_class β]
[has_continuous_add β]
(f g : zero_at_infty_continuous_map α β) :
@[protected, instance]
def
zero_at_infty_continuous_map.add_zero_class
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_zero_class β]
[has_continuous_add β] :
Equations
- zero_at_infty_continuous_map.add_zero_class = function.injective.add_zero_class coe_fn zero_at_infty_continuous_map.add_zero_class._proof_1 zero_at_infty_continuous_map.add_zero_class._proof_2 zero_at_infty_continuous_map.coe_add
@[simp]
theorem
zero_at_infty_continuous_map.coe_nsmul_rec
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β]
(f : zero_at_infty_continuous_map α β)
(n : ℕ) :
@[protected, instance]
def
zero_at_infty_continuous_map.has_nat_scalar
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β] :
Equations
- zero_at_infty_continuous_map.has_nat_scalar = {smul := λ (n : ℕ) (f : zero_at_infty_continuous_map α β), {to_continuous_map := n • ↑f, zero_at_infty' := _}}
@[protected, instance]
def
zero_at_infty_continuous_map.add_monoid
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β] :
Equations
- zero_at_infty_continuous_map.add_monoid = function.injective.add_monoid coe_fn zero_at_infty_continuous_map.add_monoid._proof_1 zero_at_infty_continuous_map.add_monoid._proof_2 zero_at_infty_continuous_map.add_monoid._proof_3 zero_at_infty_continuous_map.add_monoid._proof_4
@[protected, instance]
def
zero_at_infty_continuous_map.add_comm_monoid
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_comm_monoid β]
[has_continuous_add β] :
Equations
- zero_at_infty_continuous_map.add_comm_monoid = function.injective.add_comm_monoid coe_fn zero_at_infty_continuous_map.add_comm_monoid._proof_1 zero_at_infty_continuous_map.add_comm_monoid._proof_2 zero_at_infty_continuous_map.add_comm_monoid._proof_3 zero_at_infty_continuous_map.add_comm_monoid._proof_4
@[protected, instance]
def
zero_at_infty_continuous_map.has_neg
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
Equations
- zero_at_infty_continuous_map.has_neg = {neg := λ (f : zero_at_infty_continuous_map α β), {to_continuous_map := -↑f, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_neg
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β]
(f : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.neg_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α)
[add_group β]
[topological_add_group β]
(f : zero_at_infty_continuous_map α β) :
@[protected, instance]
def
zero_at_infty_continuous_map.has_sub
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
Equations
- zero_at_infty_continuous_map.has_sub = {sub := λ (f g : zero_at_infty_continuous_map α β), {to_continuous_map := ↑f - ↑g, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_sub
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β]
(f g : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.sub_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α)
[add_group β]
[topological_add_group β]
(f g : zero_at_infty_continuous_map α β) :
@[simp]
theorem
zero_at_infty_continuous_map.coe_zsmul_rec
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β]
(f : zero_at_infty_continuous_map α β)
(z : ℤ) :
@[protected, instance]
def
zero_at_infty_continuous_map.has_int_scalar
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
Equations
- zero_at_infty_continuous_map.has_int_scalar = {smul := λ (n : ℤ) (f : zero_at_infty_continuous_map α β), {to_continuous_map := n • ↑f, zero_at_infty' := _}}
@[protected, instance]
def
zero_at_infty_continuous_map.add_group
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
Equations
- zero_at_infty_continuous_map.add_group = function.injective.add_group coe_fn zero_at_infty_continuous_map.add_group._proof_1 zero_at_infty_continuous_map.add_group._proof_2 zero_at_infty_continuous_map.add_group._proof_3 zero_at_infty_continuous_map.coe_neg zero_at_infty_continuous_map.coe_sub zero_at_infty_continuous_map.add_group._proof_4 zero_at_infty_continuous_map.add_group._proof_5
@[protected, instance]
def
zero_at_infty_continuous_map.add_comm_group
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_comm_group β]
[topological_add_group β] :
Equations
- zero_at_infty_continuous_map.add_comm_group = function.injective.add_comm_group coe_fn zero_at_infty_continuous_map.add_comm_group._proof_3 zero_at_infty_continuous_map.add_comm_group._proof_4 zero_at_infty_continuous_map.add_comm_group._proof_5 zero_at_infty_continuous_map.add_comm_group._proof_6 zero_at_infty_continuous_map.add_comm_group._proof_7 zero_at_infty_continuous_map.add_comm_group._proof_8 zero_at_infty_continuous_map.add_comm_group._proof_9
@[protected, instance]
def
zero_at_infty_continuous_map.has_smul
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{R : Type u_1}
[has_zero R]
[smul_with_zero R β]
[has_continuous_const_smul R β] :
has_smul R (zero_at_infty_continuous_map α β)
Equations
- zero_at_infty_continuous_map.has_smul = {smul := λ (r : R) (f : zero_at_infty_continuous_map α β), {to_continuous_map := r • ↑f, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_smul
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{R : Type u_1}
[has_zero R]
[smul_with_zero R β]
[has_continuous_const_smul R β]
(r : R)
(f : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.smul_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{R : Type u_1}
[has_zero R]
[smul_with_zero R β]
[has_continuous_const_smul R β]
(r : R)
(f : zero_at_infty_continuous_map α β)
(x : α) :
@[protected, instance]
def
zero_at_infty_continuous_map.is_central_scalar
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{R : Type u_1}
[has_zero R]
[smul_with_zero R β]
[smul_with_zero Rᵐᵒᵖ β]
[has_continuous_const_smul R β]
[is_central_scalar R β] :
@[protected, instance]
def
zero_at_infty_continuous_map.smul_with_zero
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{R : Type u_1}
[has_zero R]
[smul_with_zero R β]
[has_continuous_const_smul R β] :
Equations
- zero_at_infty_continuous_map.smul_with_zero = function.injective.smul_with_zero {to_fun := coe_fn zero_at_infty_continuous_map.has_coe_to_fun, map_zero' := _} zero_at_infty_continuous_map.smul_with_zero._proof_1 zero_at_infty_continuous_map.coe_smul
@[protected, instance]
def
zero_at_infty_continuous_map.mul_action_with_zero
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[has_zero β]
{R : Type u_1}
[monoid_with_zero R]
[mul_action_with_zero R β]
[has_continuous_const_smul R β] :
Equations
- zero_at_infty_continuous_map.mul_action_with_zero = function.injective.mul_action_with_zero {to_fun := coe_fn zero_at_infty_continuous_map.has_coe_to_fun, map_zero' := _} zero_at_infty_continuous_map.mul_action_with_zero._proof_1 zero_at_infty_continuous_map.mul_action_with_zero._proof_2
@[protected, instance]
def
zero_at_infty_continuous_map.module
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_comm_monoid β]
[has_continuous_add β]
{R : Type u_1}
[semiring R]
[module R β]
[has_continuous_const_smul R β] :
module R (zero_at_infty_continuous_map α β)
Equations
- zero_at_infty_continuous_map.module = function.injective.module R {to_fun := coe_fn zero_at_infty_continuous_map.has_coe_to_fun, map_zero' := _, map_add' := _} zero_at_infty_continuous_map.module._proof_3 zero_at_infty_continuous_map.module._proof_4
@[protected, instance]
def
zero_at_infty_continuous_map.non_unital_non_assoc_semiring
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[non_unital_non_assoc_semiring β]
[topological_semiring β] :
Equations
- zero_at_infty_continuous_map.non_unital_non_assoc_semiring = function.injective.non_unital_non_assoc_semiring coe_fn zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_2 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_3 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_4 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_5 zero_at_infty_continuous_map.non_unital_non_assoc_semiring._proof_6
@[protected, instance]
def
zero_at_infty_continuous_map.non_unital_semiring
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[non_unital_semiring β]
[topological_semiring β] :
Equations
- zero_at_infty_continuous_map.non_unital_semiring = function.injective.non_unital_semiring coe_fn zero_at_infty_continuous_map.non_unital_semiring._proof_4 zero_at_infty_continuous_map.non_unital_semiring._proof_5 zero_at_infty_continuous_map.non_unital_semiring._proof_6 zero_at_infty_continuous_map.non_unital_semiring._proof_7 zero_at_infty_continuous_map.non_unital_semiring._proof_8
@[protected, instance]
def
zero_at_infty_continuous_map.non_unital_comm_semiring
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[non_unital_comm_semiring β]
[topological_semiring β] :
Equations
- zero_at_infty_continuous_map.non_unital_comm_semiring = function.injective.non_unital_comm_semiring coe_fn zero_at_infty_continuous_map.non_unital_comm_semiring._proof_4 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_5 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_6 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_7 zero_at_infty_continuous_map.non_unital_comm_semiring._proof_8
@[protected, instance]
def
zero_at_infty_continuous_map.non_unital_non_assoc_ring
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[non_unital_non_assoc_ring β]
[topological_ring β] :
Equations
- zero_at_infty_continuous_map.non_unital_non_assoc_ring = function.injective.non_unital_non_assoc_ring coe_fn zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_5 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_6 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_7 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_8 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_9 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_10 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_11 zero_at_infty_continuous_map.non_unital_non_assoc_ring._proof_12
@[protected, instance]
def
zero_at_infty_continuous_map.non_unital_ring
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[non_unital_ring β]
[topological_ring β] :
Equations
- zero_at_infty_continuous_map.non_unital_ring = function.injective.non_unital_ring coe_fn zero_at_infty_continuous_map.non_unital_ring._proof_7 zero_at_infty_continuous_map.non_unital_ring._proof_8 zero_at_infty_continuous_map.non_unital_ring._proof_9 zero_at_infty_continuous_map.non_unital_ring._proof_10 zero_at_infty_continuous_map.non_unital_ring._proof_11 zero_at_infty_continuous_map.non_unital_ring._proof_12 zero_at_infty_continuous_map.non_unital_ring._proof_13 zero_at_infty_continuous_map.non_unital_ring._proof_14
@[protected, instance]
def
zero_at_infty_continuous_map.non_unital_comm_ring
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[non_unital_comm_ring β]
[topological_ring β] :
Equations
- zero_at_infty_continuous_map.non_unital_comm_ring = function.injective.non_unital_comm_ring coe_fn zero_at_infty_continuous_map.non_unital_comm_ring._proof_7 zero_at_infty_continuous_map.non_unital_comm_ring._proof_8 zero_at_infty_continuous_map.non_unital_comm_ring._proof_9 zero_at_infty_continuous_map.non_unital_comm_ring._proof_10 zero_at_infty_continuous_map.non_unital_comm_ring._proof_11 zero_at_infty_continuous_map.non_unital_comm_ring._proof_12 zero_at_infty_continuous_map.non_unital_comm_ring._proof_13 zero_at_infty_continuous_map.non_unital_comm_ring._proof_14
@[protected, instance]
def
zero_at_infty_continuous_map.is_scalar_tower
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{R : Type u_1}
[semiring R]
[non_unital_non_assoc_semiring β]
[topological_semiring β]
[module R β]
[has_continuous_const_smul R β]
[is_scalar_tower R β β] :
@[protected, instance]
def
zero_at_infty_continuous_map.smul_comm_class
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{R : Type u_1}
[semiring R]
[non_unital_non_assoc_semiring β]
[topological_semiring β]
[module R β]
[has_continuous_const_smul R β]
[smul_comm_class R β β] :
theorem
zero_at_infty_continuous_map.uniform_continuous
{F : Type u_1}
{β : Type v}
{γ : Type w}
[uniform_space β]
[uniform_space γ]
[has_zero γ]
[zero_at_infty_continuous_map_class F β γ]
(f : F) :
Metric structure #
When β is a metric space, then every element of C₀(α, β) is bounded, and so there is a natural
inclusion map zero_at_infty_continuous_map.to_bcf : C₀(α, β) → (α →ᵇ β). Via this map C₀(α, β)
inherits a metric as the pullback of the metric on α →ᵇ β. Moreover, this map has closed range
in α →ᵇ β and consequently C₀(α, β) is a complete space whenever β is complete.
@[protected]
theorem
zero_at_infty_continuous_map.bounded
{F : Type u_1}
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
[zero_at_infty_continuous_map_class F α β]
(f : F) :
theorem
zero_at_infty_continuous_map.bounded_range
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.bounded_image
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β)
(s : set α) :
metric.bounded (⇑f '' s)
@[protected, instance]
def
zero_at_infty_continuous_map.bounded_continuous_map_class
{F : Type u_1}
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
[zero_at_infty_continuous_map_class F α β] :
Equations
- zero_at_infty_continuous_map.bounded_continuous_map_class = {coe := zero_at_infty_continuous_map_class.coe _inst_4, coe_injective' := _, map_continuous := _, map_bounded := _}
def
zero_at_infty_continuous_map.to_bcf
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β) :
Construct a bounded continuous function from a continuous function vanishing at infinity.
Equations
- f.to_bcf = {to_continuous_map := ↑f, map_bounded' := _}
@[simp]
theorem
zero_at_infty_continuous_map.to_bcf_apply
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β)
(a : α) :
@[simp]
theorem
zero_at_infty_continuous_map.to_bcf_to_continuous_map
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
(f : zero_at_infty_continuous_map α β) :
theorem
zero_at_infty_continuous_map.to_bcf_injective
(α : Type u)
(β : Type v)
[topological_space α]
[metric_space β]
[has_zero β] :
@[protected, instance]
noncomputable
def
zero_at_infty_continuous_map.metric_space
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β] :
The type of continuous functions vanishing at infinity, with the uniform distance induced by the
inclusion zero_at_infinity_continuous_map.to_bcf, is a metric space.
@[simp]
theorem
zero_at_infty_continuous_map.dist_to_bcf_eq_dist
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
{f g : zero_at_infty_continuous_map α β} :
has_dist.dist f.to_bcf g.to_bcf = has_dist.dist f g
theorem
zero_at_infty_continuous_map.tendsto_iff_tendsto_uniformly
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
{ι : Type u_1}
{F : ι → zero_at_infty_continuous_map α β}
{f : zero_at_infty_continuous_map α β}
{l : filter ι} :
filter.tendsto F l (nhds f) ↔ tendsto_uniformly (λ (i : ι), ⇑(F i)) ⇑f l
Convergence in the metric on C₀(α, β) is uniform convergence.
theorem
zero_at_infty_continuous_map.isometry_to_bcf
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β] :
theorem
zero_at_infty_continuous_map.closed_range_to_bcf
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β] :
@[protected, instance]
def
zero_at_infty_continuous_map.complete_space
{α : Type u}
{β : Type v}
[topological_space α]
[metric_space β]
[has_zero β]
[complete_space β] :
Continuous functions vanishing at infinity taking values in a complete space form a complete space.
Normed space #
The norm structure on C₀(α, β) is the one induced by the inclusion to_bcf : C₀(α, β) → (α →ᵇ b),
viewed as an additive monoid homomorphism. Then C₀(α, β) is naturally a normed space over a normed
field 𝕜 whenever β is as well.
@[protected, instance]
noncomputable
def
zero_at_infty_continuous_map.normed_add_comm_group
{α : Type u}
{β : Type v}
[topological_space α]
[normed_add_comm_group β] :
Equations
- zero_at_infty_continuous_map.normed_add_comm_group = normed_add_comm_group.induced (zero_at_infty_continuous_map α β) (bounded_continuous_function α β) {to_fun := zero_at_infty_continuous_map.to_bcf (add_zero_class.to_has_zero β), map_zero' := _, map_add' := _} zero_at_infty_continuous_map.normed_add_comm_group._proof_6
@[simp]
theorem
zero_at_infty_continuous_map.norm_to_bcf_eq_norm
{α : Type u}
{β : Type v}
[topological_space α]
[normed_add_comm_group β]
{f : zero_at_infty_continuous_map α β} :
@[protected, instance]
def
zero_at_infty_continuous_map.normed_space
{α : Type u}
{β : Type v}
[topological_space α]
[normed_add_comm_group β]
{𝕜 : Type u_2}
[normed_field 𝕜]
[normed_space 𝕜 β] :
Equations
- zero_at_infty_continuous_map.normed_space = {to_module := zero_at_infty_continuous_map.module zero_at_infty_continuous_map.normed_space._proof_2, norm_smul_le := _}
@[protected, instance]
noncomputable
def
zero_at_infty_continuous_map.non_unital_normed_ring
{α : Type u}
{β : Type v}
[topological_space α]
[non_unital_normed_ring β] :
Equations
- zero_at_infty_continuous_map.non_unital_normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm zero_at_infty_continuous_map.normed_add_comm_group, to_non_unital_ring := {add := non_unital_ring.add zero_at_infty_continuous_map.non_unital_ring, add_assoc := _, zero := non_unital_ring.zero zero_at_infty_continuous_map.non_unital_ring, zero_add := _, add_zero := _, nsmul := non_unital_ring.nsmul zero_at_infty_continuous_map.non_unital_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg zero_at_infty_continuous_map.non_unital_ring, sub := non_unital_ring.sub zero_at_infty_continuous_map.non_unital_ring, sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul zero_at_infty_continuous_map.non_unital_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_ring.mul zero_at_infty_continuous_map.non_unital_ring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}, to_metric_space := normed_add_comm_group.to_metric_space zero_at_infty_continuous_map.normed_add_comm_group, dist_eq := _, norm_mul := _}
Star structure #
It is possible to equip C₀(α, β) with a pointwise star operation whenever there is a continuous
star : β → β for which star (0 : β) = 0. We don't have quite this weak a typeclass, but
star_add_monoid is close enough.
The star_add_monoid and normed_star_group classes on C₀(α, β) are inherited from their
counterparts on α →ᵇ β. Ultimately, when β is a C⋆-ring, then so is C₀(α, β).
@[protected, instance]
def
zero_at_infty_continuous_map.has_star
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[star_add_monoid β]
[has_continuous_star β] :
Equations
- zero_at_infty_continuous_map.has_star = {star := λ (f : zero_at_infty_continuous_map α β), {to_continuous_map := {to_fun := λ (x : α), has_star.star (⇑f x), continuous_to_fun := _}, zero_at_infty' := _}}
@[simp]
theorem
zero_at_infty_continuous_map.coe_star
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[star_add_monoid β]
[has_continuous_star β]
(f : zero_at_infty_continuous_map α β) :
⇑(has_star.star f) = has_star.star ⇑f
theorem
zero_at_infty_continuous_map.star_apply
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[star_add_monoid β]
[has_continuous_star β]
(f : zero_at_infty_continuous_map α β)
(x : α) :
⇑(has_star.star f) x = has_star.star (⇑f x)
@[protected, instance]
def
zero_at_infty_continuous_map.star_add_monoid
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[add_monoid β]
[star_add_monoid β]
[has_continuous_star β]
[has_continuous_add β] :
Equations
@[protected, instance]
def
zero_at_infty_continuous_map.normed_star_group
{α : Type u}
{β : Type v}
[topological_space α]
[normed_add_comm_group β]
[star_add_monoid β]
[normed_star_group β] :
@[protected, instance]
def
zero_at_infty_continuous_map.star_module
{α : Type u}
{β : Type v}
[topological_space α]
{𝕜 : Type u_2}
[has_zero 𝕜]
[has_star 𝕜]
[add_monoid β]
[star_add_monoid β]
[topological_space β]
[has_continuous_star β]
[smul_with_zero 𝕜 β]
[has_continuous_const_smul 𝕜 β]
[star_module 𝕜 β] :
@[protected, instance]
def
zero_at_infty_continuous_map.star_ring
{α : Type u}
{β : Type v}
[topological_space α]
[non_unital_semiring β]
[star_ring β]
[topological_space β]
[has_continuous_star β]
[topological_semiring β] :
@[protected, instance]
def
zero_at_infty_continuous_map.cstar_ring
{α : Type u}
{β : Type v}
[topological_space α]
[non_unital_normed_ring β]
[star_ring β]
[cstar_ring β] :
C₀ as a functor #
For each β with sufficient structure, there is a contravariant functor C₀(-, β) from the
category of topological spaces with morphisms given by cocompact_maps.
def
zero_at_infty_continuous_map.comp
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[has_zero δ]
(f : zero_at_infty_continuous_map γ δ)
(g : cocompact_map β γ) :
Composition of a continuous function vanishing at infinity with a cocompact map yields another continuous function vanishing at infinity.
Equations
- f.comp g = {to_continuous_map := ↑f.comp ↑g, zero_at_infty' := _}
@[simp]
theorem
zero_at_infty_continuous_map.coe_comp_to_continuous_fun
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[has_zero δ]
(f : zero_at_infty_continuous_map γ δ)
(g : cocompact_map β γ) :
@[simp]
theorem
zero_at_infty_continuous_map.comp_id
{γ : Type w}
{δ : Type u_2}
[topological_space γ]
[topological_space δ]
[has_zero δ]
(f : zero_at_infty_continuous_map γ δ) :
f.comp (cocompact_map.id γ) = f
@[simp]
theorem
zero_at_infty_continuous_map.comp_assoc
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[has_zero δ]
(f : zero_at_infty_continuous_map γ δ)
(g : cocompact_map β γ)
(h : cocompact_map α β) :
@[simp]
theorem
zero_at_infty_continuous_map.zero_comp
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[has_zero δ]
(g : cocompact_map β γ) :
def
zero_at_infty_continuous_map.comp_add_monoid_hom
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[add_monoid δ]
[has_continuous_add δ]
(g : cocompact_map β γ) :
Composition as an additive monoid homomorphism.
Equations
- zero_at_infty_continuous_map.comp_add_monoid_hom g = {to_fun := λ (f : zero_at_infty_continuous_map γ δ), f.comp g, map_zero' := _, map_add' := _}
def
zero_at_infty_continuous_map.comp_mul_hom
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[mul_zero_class δ]
[has_continuous_mul δ]
(g : cocompact_map β γ) :
Composition as a semigroup homomorphism.
Equations
- zero_at_infty_continuous_map.comp_mul_hom g = {to_fun := λ (f : zero_at_infty_continuous_map γ δ), f.comp g, map_mul' := _}
def
zero_at_infty_continuous_map.comp_linear_map
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
[add_comm_monoid δ]
[has_continuous_add δ]
{R : Type u_1}
[semiring R]
[module R δ]
[has_continuous_const_smul R δ]
(g : cocompact_map β γ) :
Composition as a linear map.
Equations
- zero_at_infty_continuous_map.comp_linear_map g = {to_fun := λ (f : zero_at_infty_continuous_map γ δ), f.comp g, map_add' := _, map_smul' := _}
def
zero_at_infty_continuous_map.comp_non_unital_alg_hom
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[topological_space β]
[topological_space γ]
[topological_space δ]
{R : Type u_1}
[semiring R]
[non_unital_non_assoc_semiring δ]
[topological_semiring δ]
[module R δ]
[has_continuous_const_smul R δ]
(g : cocompact_map β γ) :
Composition as a non-unital algebra homomorphism.
Equations
- zero_at_infty_continuous_map.comp_non_unital_alg_hom g = {to_fun := λ (f : zero_at_infty_continuous_map γ δ), f.comp g, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _}