Documentation

Mathlib.Topology.Bornology.Hom

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 #

Typeclasses #

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.

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

    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} [FunLike F α β] [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (f : F) {s : Set α} (hs : IsBounded s) :
      IsBounded (f '' s)
      def LocallyBoundedMapClass.toLocallyBoundedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (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 α β.

      Equations
        Instances For
          instance instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] :
          Equations
            instance LocallyBoundedMap.instFunLike {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] :
            Equations
              theorem LocallyBoundedMap.ext {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] {f g : LocallyBoundedMap α β} (h : ∀ (a : α), f a = g a) :
              f = g
              theorem LocallyBoundedMap.ext_iff {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] {f g : LocallyBoundedMap α β} :
              f = g ∀ (a : α), f a = g a
              def LocallyBoundedMap.copy {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) (f' : αβ) (h : f' = f) :

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

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

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

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

                      id as a LocallyBoundedMap.

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

                          Composition of LocallyBoundedMaps as a LocallyBoundedMap.

                          Equations
                            Instances For
                              @[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
                              @[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)
                              @[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)
                              @[simp]
                              theorem LocallyBoundedMap.comp_id {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) :
                              @[simp]
                              theorem LocallyBoundedMap.id_comp {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) :
                              @[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₂
                              @[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₂