measurable_piEquivPiSubtypeProd — Mathlib

English

The piEquivPiSubtypeProd with predicate p is measurable.

Русский

Эквивалентность piEquivPiSubtypeProd с предикатом p измерима.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{Equiv.piEquivPiSubtypeProd}\\, p\\ X$)$$

Lean4

@[measurability]
theorem measurable_piEquivPiSubtypeProd (p : δ → Prop) [DecidablePred p] :
    Measurable (Equiv.piEquivPiSubtypeProd p X) :=
  (measurable_pi_iff.2 fun _ => measurable_pi_apply _).prodMk (measurable_pi_iff.2 fun _ => measurable_pi_apply _)

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