Binary Products of Quasi-Borel Spaces

This file defines binary products of quasi-borel spaces by giving a QuasiBorelSpace instance for the · × · type.

See [HKSY17], Proposition 16.

instance QuasiBorelSpace.Prod.instProd {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : QuasiBorelSpace (A × B)

Equations

• One or more equations did not get rendered due to their size.

theorem QuasiBorelSpace.Prod.isHom_def {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] (f : ℝ → A × B) : IsHom f ↔ (IsHom fun (x : ℝ) => (f x).1) ∧ IsHom fun (x : ℝ) => (f x).2

@[simp]

theorem QuasiBorelSpace.Prod.isHom_fst {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom Prod.fst

theorem QuasiBorelSpace.Prod.isHom_fst' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → B × C} (hf : IsHom f) : IsHom fun (x : A) => (f x).1

@[simp]

theorem QuasiBorelSpace.Prod.isHom_snd {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom Prod.snd

theorem QuasiBorelSpace.Prod.isHom_snd' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → B × C} (hf : IsHom f) : IsHom fun (x : A) => (f x).2

theorem QuasiBorelSpace.Prod.isHom_mk {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → B} (hf : IsHom f) {g : A → C} (hg : IsHom g) : IsHom fun (x : A) => (f x, g x)

@[simp]

theorem QuasiBorelSpace.Prod.isHom_iff {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] (f : A → B × C) : IsHom f ↔ (IsHom fun (x : A) => (f x).1) ∧ IsHom fun (x : A) => (f x).2

instance QuasiBorelSpace.Prod.instMeasurableQuasiBorelSpaceProd {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [MeasurableSpace A] [MeasurableSpace B] [MeasurableQuasiBorelSpace A] [MeasurableQuasiBorelSpace B] : MeasurableQuasiBorelSpace (A × B)

theorem QuasiBorelSpace.Prod.isHom_map {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {D : Type u_4} [QuasiBorelSpace D] {f : A → B} {g : C → D} (hf : IsHom f) (hg : IsHom g) : IsHom (Prod.map f g)

theorem QuasiBorelSpace.Prod.isHom_of_uncurry {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {D : Type u_4} [QuasiBorelSpace D] {f : A → B → C} (hf : IsHom (Function.uncurry f)) {g : D → A} (hg : IsHom g) {h : D → B} (hh : IsHom h) : IsHom fun (x : D) => f (g x) (h x)

theorem QuasiBorelSpace.Prod.isHom_fst_comp {α : Type u_5} {β : Type u_6} [QuasiBorelSpace α] [QuasiBorelSpace β] {f : ℝ → α × β} (hf : IsHom f) : IsHom fun (r : ℝ) => (f r).1

theorem QuasiBorelSpace.Prod.isHom_snd_comp {α : Type u_5} {β : Type u_6} [QuasiBorelSpace α] [QuasiBorelSpace β] {f : ℝ → α × β} (hf : IsHom f) : IsHom fun (r : ℝ) => (f r).2