English
The symmetric of the piEquivPiSubtypeProd with predicate p is Measurable.
Русский
Симметрическая часть piEquivPiSubtypeProd с предикатом p измерима.
LaTeX
$$$\\mathrm{Measurable}(\\mathrm{Equiv.piEquivPiSubtypeProd}\\, p\\ X)\\.\\mathrm{symm}$$$
Lean4
@[measurability]
theorem measurable_piEquivPiSubtypeProd_symm (p : δ → Prop) [DecidablePred p] :
Measurable (Equiv.piEquivPiSubtypeProd p X).symm :=
by
refine measurable_pi_iff.2 fun j => ?_
by_cases hj : p j
· simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]
have : Measurable fun (f : ∀ i : { x // p x }, X i.1) => f ⟨j, hj⟩ :=
measurable_pi_apply (X := fun i : { x // p x } => X i.1) ⟨j, hj⟩
exact Measurable.comp this measurable_fst
· simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]
have : Measurable fun (f : ∀ i : { x // ¬p x }, X i.1) => f ⟨j, hj⟩ :=
measurable_pi_apply (X := fun i : { x // ¬p x } => X i.1) ⟨j, hj⟩
exact Measurable.comp this measurable_snd
