# Locally bounded maps #

This file defines locally bounded maps between bornologies.

We use the `DFunLike` 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`

source
structure LocallyBoundedMap (α : 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.

- toFun : α → β

  The function underlying a locally bounded map

- comap_cobounded_le' : Filter.comap self.toFun (Bornology.cobounded β) ≤ Bornology.cobounded α

  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.

Instances For

source
class LocallyBoundedMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Bornology α] [Bornology β] [FunLike F α β] :
Prop

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

You should extend this class when you extend `LocallyBoundedMap`.

- comap_cobounded_le (f : F) : Filter.comap (⇑f) (Bornology.cobounded β) ≤ Bornology.cobounded α

  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.

Instances

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

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 α β`.

Equations

- ↑f = { toFun := ⇑f, comap_cobounded_le' := ⋯ }

Instances For

source
instance instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] :
CoeTC F (LocallyBoundedMap α β)
Equations

- instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass = { coe := fun (f : F) => { toFun := ⇑f, comap_cobounded_le' := ⋯ } }

source
instance LocallyBoundedMap.instFunLike {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] :
FunLike (LocallyBoundedMap α β) α β
Equations

- LocallyBoundedMap.instFunLike = { coe := fun (f : LocallyBoundedMap α β) => f.toFun, coe_injective' := ⋯ }

source
instance LocallyBoundedMap.instLocallyBoundedMapClass {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] :
LocallyBoundedMapClass (LocallyBoundedMap α β) α β
source
theorem LocallyBoundedMap.ext {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] {f g : LocallyBoundedMap α β} (h : ∀ (a : α), f a = g a) :
f = g
source
theorem LocallyBoundedMap.ext_iff {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] {f g : LocallyBoundedMap α β} :
f = g ↔ ∀ (a : α), f a = g a
source
def LocallyBoundedMap.copy {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = ⇑f) :
LocallyBoundedMap α β

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

Equations

- f.copy f' h = { toFun := f', comap_cobounded_le' := ⋯ }

Instances For

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

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

Equations

- LocallyBoundedMap.ofMapBounded f h = { toFun := f, comap_cobounded_le' := ⋯ }

Instances For

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

`id` as a `LocallyBoundedMap`.

Equations

- LocallyBoundedMap.id α = { toFun := id, comap_cobounded_le' := ⋯ }

Instances For

source
instance LocallyBoundedMap.instInhabited (α : Type u_2) [Bornology α] :
Inhabited (LocallyBoundedMap α α)
Equations

- LocallyBoundedMap.instInhabited α = { default := LocallyBoundedMap.id α }

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

Composition of `LocallyBoundedMap`s as a `LocallyBoundedMap`.

Equations

- f.comp g = { toFun := ⇑f ∘ ⇑g, comap_cobounded_le' := ⋯ }

Instances For

source
@[simp]
theorem LocallyBoundedMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem LocallyBoundedMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) (a : α) :
(f.comp g) a = f (g a)
source
@[simp]
theorem LocallyBoundedMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Bornology α] [Bornology β] [Bornology γ] [Bornology δ] (f : LocallyBoundedMap γ δ) (g : LocallyBoundedMap β γ) (h : LocallyBoundedMap α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem LocallyBoundedMap.comp_id {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) :
f.comp (LocallyBoundedMap.id α) = f
source
@[simp]
theorem LocallyBoundedMap.id_comp {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) :
(LocallyBoundedMap.id β).comp f = f
source
@[simp]
theorem LocallyBoundedMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] {g₁ g₂ : LocallyBoundedMap β γ} {f : LocallyBoundedMap α β} (hf : Function.Surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
@[simp]
theorem LocallyBoundedMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] {g : LocallyBoundedMap β γ} {f₁ f₂ : LocallyBoundedMap α β} (hg : Function.Injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂