Exponentials of Quasi-Borel Spaces

This file defines the exponential object in the category of quasi-borel spaces.

See [HKSY17], Proposition 18.

structure QuasiBorelHom (A : Type u_1) (B : Type u_2) [QuasiBorelSpace A] [QuasiBorelSpace B] : Type (max u_1 u_2)

The type of morphisms between QuasiBorelSpaces.

• toFun : A → B

  The underlying function.

• property : QuasiBorelSpace.IsHom self.toFun

  The underlying function is a morphism.

def QuasiBorelHom.«term_→𝒒_» : Lean.TrailingParserDescr

The type of morphisms between QuasiBorelSpaces.

Equations

• QuasiBorelHom.«term_→𝒒_» = Lean.ParserDescr.trailingNode `QuasiBorelHom.«term_→𝒒_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →𝒒 ") (Lean.ParserDescr.cat `term 25))

@[instance_reducible]

instance QuasiBorelHom.instFunLike {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] : FunLike (A →𝒒 B) A B

Equations

• QuasiBorelHom.instFunLike = { coe := QuasiBorelHom.toFun, coe_injective := ⋯ }

def QuasiBorelHom.Simps.coe {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A →𝒒 B) : A → B

A simps projection for function coercion.

Equations

• QuasiBorelHom.Simps.coe f = ⇑f

def QuasiBorelHom.copy {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (f : A →𝒒 B) (f' : A → B) (h : f' = ⇑f) : A →𝒒 B

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

Equations

• f.copy f' h = { toFun := f', property := ⋯ }

@[instance_reducible]

instance QuasiBorelHom.instQuasiBorelSpace {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : QuasiBorelSpace (A →𝒒 B)

Equations

• QuasiBorelHom.instQuasiBorelSpace = { IsVar := fun (φ : ℝ → A →𝒒 B) => QuasiBorelSpace.IsHom fun (x : ℝ × A) => (φ x.1) x.2, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

@[instance_reducible]

instance QuasiBorelHom.instMeasurableSpace {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : MeasurableSpace (A →𝒒 B)

Equations

• QuasiBorelHom.instMeasurableSpace = QuasiBorelSpace.toMeasurableSpace

@[instance_reducible]

instance QuasiBorelHom.instSetoid {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} [Setoid B] : Setoid (A →𝒒 B)

Equations

• QuasiBorelHom.instSetoid = { r := fun (f g : A →𝒒 B) => ∀ (x : A), f x ≈ g x, iseqv := ⋯ }