fst_map_prod — Mathlib

English

If κ : Kernel α β, and f,g: β → γ with g measurable, then fst (κ.map (x ↦ (f x, g x))) = κ.map f.

Русский

Если κ : Kernel α β, и f,g: β → γ, причём g измерима, тогда fst (κ.map (x ↦ (f x, g x))) = κ.map f.

LaTeX

$$$$\\text{fst}(\\kappa.map(\\lambda x. (f x, g x))) = \\text{map }\\kappa f$$$$

Lean4

theorem fst_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} (hg : Measurable g) :
    fst (map κ (fun x ↦ (f x, g x))) = map κ f :=
  by
  by_cases hf : Measurable f
  · ext x s hs
    rw [fst_apply' _ _ hs, map_apply' _ (hf.prod hg) _, map_apply' _ hf _ hs]
    · simp only [Set.preimage, Set.mem_setOf]
    · exact measurable_fst hs
  · have : ¬Measurable (fun x ↦ (f x, g x)) := by contrapose! hf; exact hf.fst
    simp [map_of_not_measurable _ hf, map_of_not_measurable _ this]

Похожие утверждения