Documentation

QuasiBorelSpaces.Hom.Constructions

Exponentials of Quasi-Borel Spaces #

This file provides QuasiBorelHom constructions.

source
noncomputable def QuasiBorelHom.mk' {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A โ†’ B) :
A โ†’๐’’ B
Equations
Instances For
    source
    @[simp]
    theorem QuasiBorelHom.mk'_eq {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {f : A โ†’ B} (hf : QuasiBorelSpace.IsHom f) :
    mk' f = { toFun := f, property := hf }
    source
    def QuasiBorelHom.curry {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A ร— B โ†’๐’’ C) :
    A โ†’๐’’ B โ†’๐’’ C

    Currying for QuasiBorelHoms.

    Equations
    • f.curry = { toFun := fun (x : A) => { toFun := fun (y : B) => f (x, y), property := โ‹ฏ }, property := โ‹ฏ }
    Instances For
      source
      @[simp]
      theorem QuasiBorelHom.curry_coe_coe {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A ร— B โ†’๐’’ C) (x : A) :
      โ‡‘(f.curry x) = fun (y : B) => f (x, y)
      source
      def QuasiBorelHom.uncurry {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A โ†’๐’’ B โ†’๐’’ C) :
      A ร— B โ†’๐’’ C

      Uncurrying for QuasiBorelHoms.

      Equations
      • f.uncurry = { toFun := fun (x : A ร— B) => (f x.1) x.2, property := โ‹ฏ }
      Instances For
        source
        @[simp]
        theorem QuasiBorelHom.uncurry_coe {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A โ†’๐’’ B โ†’๐’’ C) :
        โ‡‘f.uncurry = fun (x : A ร— B) => (f x.1) x.2
        source
        @[simp]
        theorem QuasiBorelHom.curry_uncurry {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {C : Type u_3} {xโœยฒ : QuasiBorelSpace C} (f : A โ†’๐’’ B โ†’๐’’ C) :
        f.uncurry.curry = f
        source
        @[simp]
        theorem QuasiBorelHom.uncurry_curry {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {C : Type u_3} {xโœยฒ : QuasiBorelSpace C} (f : A ร— B โ†’๐’’ C) :
        f.curry.uncurry = f
        source
        def QuasiBorelHom.id {A : Type u_1} [QuasiBorelSpace A] :
        A โ†’๐’’ A

        The identity morphism.

        Equations
        Instances For
          source
          @[simp]
          theorem QuasiBorelHom.id_coe {A : Type u_1} [QuasiBorelSpace A] :
          โ‡‘id = fun (x : A) => x
          source
          @[simp]
          theorem QuasiBorelHom.eq_id {A : Type u_1} {xโœ : QuasiBorelSpace A} :
          { toFun := fun (x : A) => x, property := โ‹ฏ } = id
          source
          def QuasiBorelHom.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : B โ†’๐’’ C) (g : A โ†’๐’’ B) :
          A โ†’๐’’ C

          Morphism composition.

          Equations
          • f.comp g = { toFun := fun (x : A) => f (g x), property := โ‹ฏ }
          Instances For
            source
            @[simp]
            theorem QuasiBorelHom.comp_coe {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : B โ†’๐’’ C) (g : A โ†’๐’’ B) :
            โ‡‘(f.comp g) = fun (x : A) => f (g x)
            source
            @[simp]
            theorem QuasiBorelHom.comp_mk {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {C : Type u_3} {xโœยฒ : QuasiBorelSpace C} {f : B โ†’ C} (hf : QuasiBorelSpace.IsHom f) {g : A โ†’ B} (hg : QuasiBorelSpace.IsHom g) :
            { toFun := f, property := hf }.comp { toFun := g, property := hg } = { toFun := fun (x : A) => f (g x), property := โ‹ฏ }
            source
            @[simp]
            theorem QuasiBorelHom.id_comp {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} (f : A โ†’๐’’ B) :
            id.comp f = f
            source
            @[simp]
            theorem QuasiBorelHom.comp_id {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} (f : A โ†’๐’’ B) :
            f.comp id = f
            source
            @[simp]
            theorem QuasiBorelHom.comp_assoc {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {C : Type u_3} {xโœยฒ : QuasiBorelSpace C} {D : Type u_4} {xโœยณ : QuasiBorelSpace D} (f : C โ†’๐’’ D) (g : B โ†’๐’’ C) (h : A โ†’๐’’ B) :
            (f.comp g).comp h = f.comp (g.comp h)