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 #

locally_bounded_map: Locally bounded maps. Maps which preserve boundedness.

Typeclasses #

locally_bounded_map_class

source

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

Type (max u_6 u_7)

to_fun : α → β
comap_cobounded_le' : filter.comap self.to_fun (bornology.cobounded β) ≤ bornology.cobounded α

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

Instances for locally_bounded_map

locally_bounded_map.has_sizeof_inst
locally_bounded_map.has_coe_t
locally_bounded_map.locally_bounded_map_class
locally_bounded_map.has_coe_to_fun
locally_bounded_map.inhabited

source

@[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)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective locally_bounded_map_class.coe
comap_cobounded_le : ∀ (f : F), filter.comap ⇑f (bornology.cobounded β) ≤ bornology.cobounded α

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

locally_bounded_map.locally_bounded_map_class

Instances of other typeclasses for locally_bounded_map_class

locally_bounded_map_class.has_sizeof_inst

source

@[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 : α), β)

source

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) :

bornology.is_bounded (⇑f '' s)

source

@[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 α β] :

has_coe_t F (locally_bounded_map α β)

Equations

locally_bounded_map.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, comap_cobounded_le' := _}}

source

@[protected, instance]

def locally_bounded_map.locally_bounded_map_class {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] :

locally_bounded_map_class (locally_bounded_map α β) α β

Equations

locally_bounded_map.locally_bounded_map_class = {coe := λ (f : locally_bounded_map α β), f.to_fun, coe_injective' := _, comap_cobounded_le := _}

source

@[protected, instance]

def locally_bounded_map.has_coe_to_fun {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] :

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

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

Equations

locally_bounded_map.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem locally_bounded_map.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] {f : locally_bounded_map α β} :

f.to_fun = ⇑f

source

@[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

source

@[protected]

def locally_bounded_map.copy {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) (f' : α → β) (h : f' = ⇑f) :

locally_bounded_map α β

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

Equations

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

source

@[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'

source

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

source

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)) :

locally_bounded_map α β

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

Equations

locally_bounded_map.of_map_bounded f h = {to_fun := f, comap_cobounded_le' := _}

source

@[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)} :

⇑(locally_bounded_map.of_map_bounded f h) = f

source

@[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 : α) :

⇑(locally_bounded_map.of_map_bounded f h) a = f a

source

@[protected]

def locally_bounded_map.id (α : Type u_2) [bornology α] :

locally_bounded_map α α

id as a locally_bounded_map.

Equations

locally_bounded_map.id α = {to_fun := id α, comap_cobounded_le' := _}

source

@[protected, instance]

def locally_bounded_map.inhabited (α : Type u_2) [bornology α] :

inhabited (locally_bounded_map α α)

Equations

locally_bounded_map.inhabited α = {default := locally_bounded_map.id α _inst_1}

source

@[simp]

theorem locally_bounded_map.coe_id (α : Type u_2) [bornology α] :

⇑(locally_bounded_map.id α) = id

source

@[simp]

theorem locally_bounded_map.id_apply {α : Type u_2} [bornology α] (a : α) :

⇑(locally_bounded_map.id α) a = a

source

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 α β) :

locally_bounded_map α γ

Composition of locally_bounded_maps as a locally_bounded_map.

Equations

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

source

@[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

source

@[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)

source

@[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)

source

@[simp]

theorem locally_bounded_map.comp_id {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) :

f.comp (locally_bounded_map.id α) = f

source

@[simp]

theorem locally_bounded_map.id_comp {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] (f : locally_bounded_map α β) :

(locally_bounded_map.id β).comp f = f

source

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₂

source

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₂