LeanMachineLearning exposition

MeasurableSpace.comap_pi🔗

Minimal Lean file

comap_pi🔗

LemmaMeasurableSpace.comap_pi
Details

No docstring.

🔗theorem
MeasurableSpace.comap_pi.{u_1, u_2, u_3} {δ : Type u_1}
  {X : δ → Type u_2} [m : (a : δ) → MeasurableSpace (X a)]
  {α : Type u_3} {g : α → (a : δ) → X a} :
  MeasurableSpace.comap g pi =
    ⨆ a, MeasurableSpace.comap (fun x => g x a) (m a)
MeasurableSpace.comap_pi.{u_1, u_2, u_3}
  {δ : Type u_1} {X : δ → Type u_2}
  [m : (a : δ) → MeasurableSpace (X a)]
  {α : Type u_3} {g : α → (a : δ) → X a} :
  MeasurableSpace.comap g pi =
    ⨆ a,
      MeasurableSpace.comap
        (fun x => g x a) (m a)

Code

lemma comap_pi {g : α → ∀ a, X a} : pi.comap g = ⨆ a, (m a).comap (fun x ↦ g x a)
Used by (2)

Actions: Source · Open Issue

Proof
by
  simp_rw [pi, comap_iSup, comap_comp, comp_def]