Coproduct Variables

This file provides basic lemmas about coproduct variables.

@[simp]

theorem QuasiBorelSpace.Sigma.Var.mk_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {J : Type u_4} [Encodable J] {f : J → I} {i : ℝ → J} {φ : (i : J) → ℝ → P (f i)} (hφ : ∀ (i : J), IsHom (φ i)) (hi : Measurable i) : ↑(mk f i φ hφ hi) = fun (r : ℝ) => ⟨f (i r), φ (i r) r⟩

@[simp]

theorem QuasiBorelSpace.Sigma.Var.const_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} (x : Sigma P) : ↑(const x) = fun (x_1 : ℝ) => x

@[simp]

theorem QuasiBorelSpace.Sigma.Var.comp_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {f : ℝ → ℝ} (hf : Measurable f) (x : Var I P) : ↑(comp hf x) = fun (r : ℝ) => ↑x (f r)

@[simp]

theorem QuasiBorelSpace.Sigma.Var.cases_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {ix : ℝ → ℕ} (hix : Measurable ix) (φ : ℕ → Var I P) : ↑(cases hix φ) = fun (r : ℝ) => ↑(φ (ix r)) r

@[simp]

theorem QuasiBorelSpace.Sigma.Var.distrib_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {A : Type u_3} {x✝¹ : QuasiBorelSpace A} {φ₁ : ℝ → A} (hφ₁ : IsHom φ₁) (φ₂ : Var I P) : ↑(distrib hφ₁ φ₂) = fun (r : ℝ) => ⟨(↑φ₂ r).fst, (φ₁ r, (↑φ₂ r).snd)⟩

@[simp]

theorem QuasiBorelSpace.Sigma.Var.ofMeasurable_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] [Countable I] {φ : ℝ → Sigma P} (hφ : Measurable φ) : ↑(ofMeasurable hφ) = φ

@[simp]

theorem QuasiBorelSpace.Sigma.Var.measurable_coe {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] (φ : Var I P) : Measurable ↑φ

theorem QuasiBorelSpace.Sigma.Var.isHom_index {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} (φ : Var I P) : IsHom φ.index