mathlib3 documentation

topology.bornology.hom

Locally bounded maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines locally bounded maps between bornologies.

We use the fun_like design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms #

Typeclasses #

structure locally_bounded_map (α : Type u_6) (β : Type u_7) [bornology α] [bornology β] :
Type (max u_6 u_7)

The type of bounded maps from α to β, the maps which send a bounded set to a bounded set.

Instances for locally_bounded_map
@[class]
structure locally_bounded_map_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [bornology α] [bornology β] :
Type (max u_6 u_7 u_8)

locally_bounded_map_class F α β states that F is a type of bounded maps.

You should extend this class when you extend locally_bounded_map.

Instances of this typeclass
Instances of other typeclasses for locally_bounded_map_class
  • locally_bounded_map_class.has_sizeof_inst
@[instance]
def locally_bounded_map_class.to_fun_like (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [bornology α] [bornology β] [self : locally_bounded_map_class F α β] :
fun_like F α (λ (_x : α), β)
theorem is_bounded.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] [locally_bounded_map_class F α β] {f : F} {s : set α} (hs : bornology.is_bounded s) :
@[protected, instance]
def locally_bounded_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] [locally_bounded_map_class F α β] :
Equations
@[protected, instance]
def locally_bounded_map.has_coe_to_fun {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] :

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

Equations
@[simp]
theorem locally_bounded_map.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] {f : locally_bounded_map α β} :
@[ext]
theorem locally_bounded_map.ext {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] {f g : locally_bounded_map α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def locally_bounded_map.copy {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) (f' : α β) (h : f' = f) :

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

Equations
@[simp]
theorem locally_bounded_map.coe_copy {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem locally_bounded_map.copy_eq {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
def locally_bounded_map.of_map_bounded {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : α β) (h : ⦃s : set α⦄, bornology.is_bounded s bornology.is_bounded (f '' s)) :

Construct a locally_bounded_map from the fact that the function maps bounded sets to bounded sets.

Equations
@[simp]
theorem locally_bounded_map.coe_of_map_bounded {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : α β) {h : ⦃s : set α⦄, bornology.is_bounded s bornology.is_bounded (f '' s)} :
@[simp]
theorem locally_bounded_map.of_map_bounded_apply {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : α β) {h : ⦃s : set α⦄, bornology.is_bounded s bornology.is_bounded (f '' s)} (a : α) :
@[protected, instance]
Equations
@[simp]
theorem locally_bounded_map.id_apply {α : Type u_2} [bornology α] (a : α) :
def locally_bounded_map.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [bornology α] [bornology β] [bornology γ] (f : locally_bounded_map β γ) (g : locally_bounded_map α β) :

Composition of locally_bounded_maps as a locally_bounded_map.

Equations
@[simp]
theorem locally_bounded_map.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [bornology α] [bornology β] [bornology γ] (f : locally_bounded_map β γ) (g : locally_bounded_map α β) :
(f.comp g) = f g
@[simp]
theorem locally_bounded_map.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [bornology α] [bornology β] [bornology γ] (f : locally_bounded_map β γ) (g : locally_bounded_map α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem locally_bounded_map.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [bornology α] [bornology β] [bornology γ] [bornology δ] (f : locally_bounded_map γ δ) (g : locally_bounded_map β γ) (h : locally_bounded_map α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem locally_bounded_map.comp_id {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) :
@[simp]
theorem locally_bounded_map.id_comp {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) :
theorem locally_bounded_map.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [bornology α] [bornology β] [bornology γ] {g₁ g₂ : locally_bounded_map β γ} {f : locally_bounded_map α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem locally_bounded_map.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [bornology α] [bornology β] [bornology γ] {g : locally_bounded_map β γ} {f₁ f₂ : locally_bounded_map α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂