Binary Coproducts of Quasi-Borel Spaces

This file provides basic lemmas about the QuasiBorelSpace instance for the Sum (⊕) type.

theorem QuasiBorelSpace.Sum.Encoding.isHom_inl {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Encoding.inl

theorem QuasiBorelSpace.Sum.Encoding.isHom_inr {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Encoding.inr

theorem QuasiBorelSpace.Sum.Encoding.isHom_elim {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} {f : A → C} (hf : IsHom f) {g : B → C} (hg : IsHom g) : IsHom (Encoding.elim f g)

theorem QuasiBorelSpace.Sum.isHom_encode {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Sum.encode

@[simp]

theorem QuasiBorelSpace.Sum.isHom_inl {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Sum.inl

@[simp]

theorem QuasiBorelSpace.Sum.isHom_inr {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Sum.inr

theorem QuasiBorelSpace.Sum.isHom_elim {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} {f : A → C} (hf : IsHom f) {g : B → C} (hg : IsHom g) : IsHom (Sum.elim f g)

theorem QuasiBorelSpace.Sum.isHom_elim' {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 : A → B → D} (hf : IsHom fun (x : A × B) => f x.1 x.2) {g : A → C → D} (hg : IsHom fun (x : A × C) => g x.1 x.2) {h : A → B ⊕ C} (hh : IsHom h) : IsHom fun (x : A) => Sum.elim (f x) (g x) (h x)

theorem QuasiBorelSpace.Sum.isHom_map {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} {E : Type u_5} {x✝⁴ : QuasiBorelSpace E} {f : A → B → D} (hf : IsHom fun (x : A × B) => f x.1 x.2) {g : A → C → E} (hg : IsHom fun (x : A × C) => g x.1 x.2) {h : A → B ⊕ C} (hh : IsHom h) : IsHom fun (x : A) => Sum.map (f x) (g x) (h x)

@[simp]

theorem QuasiBorelSpace.Sum.isHom_isLeft {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Sum.isLeft