Documentation

QuasiBorelSpaces.Hom.Basic

Exponentials of Quasi-Borel Spaces #

This file provides basic lemmas about the QuasiBorelSpace instance for QuasiBorelHom.

source
theorem QuasiBorelHom.ext {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {f g : A โ†’๐’’ B} (h : โˆ€ (x : A), f x = g x) :
f = g
source
theorem QuasiBorelHom.ext_iff {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {f g : A โ†’๐’’ B} :
f = g โ†” โˆ€ (x : A), f x = g x
source
@[simp]
theorem QuasiBorelHom.coe_mk {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} {f : A โ†’ B} (hf : QuasiBorelSpace.IsHom f) :
โ‡‘{ toFun := f, property := hf } = f
source
@[simp]
theorem QuasiBorelHom.eta {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} (f : A โ†’๐’’ B) :
{ toFun := โ‡‘f, property := โ‹ฏ } = f
source
@[simp]
theorem QuasiBorelHom.toFun_eq_coe {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} (f : A โ†’๐’’ B) :
f.toFun = โ‡‘f
source
@[simp]
theorem QuasiBorelHom.isHom_coe {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} (f : A โ†’๐’’ B) :
QuasiBorelSpace.IsHom โ‡‘f
source
theorem QuasiBorelHom.isHom_def {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} (ฯ† : โ„ โ†’ A โ†’๐’’ B) :
QuasiBorelSpace.IsHom ฯ† โ†” QuasiBorelSpace.IsHom fun (x : โ„ ร— A) => (ฯ† x.1) x.2
source
@[simp]
theorem QuasiBorelHom.isHom_eval {A : Type u_1} {xโœ : QuasiBorelSpace A} {B : Type u_2} {xโœยน : QuasiBorelSpace B} :
QuasiBorelSpace.IsHom fun (p : (A โ†’๐’’ B) ร— A) => p.1 p.2
source
theorem QuasiBorelHom.isHom_eval' {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} (hf : QuasiBorelSpace.IsHom f) {g : A โ†’ B} (hg : QuasiBorelSpace.IsHom g) :
QuasiBorelSpace.IsHom fun (x : A) => (f x) (g x)
source
theorem QuasiBorelHom.isHom_mk {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} (hf : QuasiBorelSpace.IsHom fun (x : A ร— B) => f x.1 x.2) :
QuasiBorelSpace.IsHom fun (x : A) => { toFun := f x, property := โ‹ฏ }
source
@[simp]
theorem QuasiBorelHom.isHom_iff {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) :
QuasiBorelSpace.IsHom f โ†” QuasiBorelSpace.IsHom fun (x : A ร— B) => (f x.1) x.2