Locally bounded maps #
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 #
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
@[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)
- to_fun_like : fun_like F α (λ (_x : α), β)
- 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
Instances of other typeclasses for locally_bounded_map_class
- locally_bounded_map_class.has_sizeof_inst
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)
@[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' := _}}
@[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 = {to_fun_like := {coe := λ (f : locally_bounded_map α β), f.to_fun, coe_injective' := _}, comap_cobounded_le := _}
@[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.
@[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
- f.copy f' h = {to_fun := f', comap_cobounded_le' := _}
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
- locally_bounded_map.of_map_bounded f h = {to_fun := f, comap_cobounded_le' := _}
@[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
@[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
@[protected]
id as a locally_bounded_map.
Equations
- locally_bounded_map.id α = {to_fun := id α, comap_cobounded_le' := _}
@[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}
@[simp]
@[simp]
theorem
locally_bounded_map.id_apply
{α : Type u_2}
[bornology α]
(a : α) :
⇑(locally_bounded_map.id α) a = 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.
@[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 α β) :
@[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 : α) :
@[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 α β) :
@[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
@[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
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) :
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) :