# Documentation

Mathlib.Topology.Bornology.Hom

# Locally bounded maps #

This file defines locally bounded maps between bornologies.

We use the FunLike 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 #

• LocallyBoundedMap: Locally bounded maps. Maps which preserve boundedness.

## Typeclasses #

• LocallyBoundedMapClass
structure LocallyBoundedMap (α : Type u_6) (β : Type u_7) [] [] :
Type (max u_6 u_7)
• toFun : αβ

The function underlying a locally bounded map

• comap_cobounded_le' : Filter.comap s.toFun ()

The pullback of the Bornology.cobounded filter under the function is contained in the cobounded filter. Equivalently, the function maps bounded sets to bounded sets.

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

Instances For
class LocallyBoundedMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• comap_cobounded_le : ∀ (f : F),

The pullback of the Bornology.cobounded filter under the function is contained in the cobounded filter. Equivalently, the function maps bounded sets to bounded sets.

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

You should extend this class when you extend LocallyBoundedMap.

Instances
theorem Bornology.IsBounded.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) {s : Set α} (hs : ) :
def LocallyBoundedMapClass.toLocallyBoundedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) :

Turn an element of a type F satisfying LocallyBoundedMapClass F α β into an actual LocallyBoundedMap. This is declared as the default coercion from F to LocallyBoundedMap α β.

Instances For
instance instCoeTCLocallyBoundedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F ()
theorem LocallyBoundedMap.ext {α : Type u_2} {β : Type u_3} [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def LocallyBoundedMap.copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :

Copy of a LocallyBoundedMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem LocallyBoundedMap.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
↑() = f'
theorem LocallyBoundedMap.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
= f
def LocallyBoundedMap.ofMapBounded {α : Type u_2} {β : Type u_3} [] [] (f : αβ) (h : ∀ ⦃s : Set α⦄, Bornology.IsBounded (f '' s)) :

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

Instances For
@[simp]
theorem LocallyBoundedMap.coe_ofMapBounded {α : Type u_2} {β : Type u_3} [] [] (f : αβ) {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded (f '' s)} :
= f
@[simp]
theorem LocallyBoundedMap.ofMapBounded_apply {α : Type u_2} {β : Type u_3} [] [] (f : αβ) {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded (f '' s)} (a : α) :
↑() a = f a
def LocallyBoundedMap.id (α : Type u_2) [] :

id as a LocallyBoundedMap.

Instances For
@[simp]
theorem LocallyBoundedMap.coe_id (α : Type u_2) [] :
↑() = id
@[simp]
theorem LocallyBoundedMap.id_apply {α : Type u_2} [] (a : α) :
↑() a = a
def LocallyBoundedMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of LocallyBoundedMaps as a LocallyBoundedMap.

Instances For
@[simp]
theorem LocallyBoundedMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
↑() = f g
@[simp]
theorem LocallyBoundedMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
↑() a = f (g a)
@[simp]
theorem LocallyBoundedMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
@[simp]
theorem LocallyBoundedMap.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem LocallyBoundedMap.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem LocallyBoundedMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g₁ : } {g₂ : } {f : } (hf : ) :
g₁ = g₂
@[simp]
theorem LocallyBoundedMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g : } {f₁ : } {f₂ : } (hg : ) :
f₁ = f₂