measurable_piCongrLeft — Mathlib

English

The symmetry (inverse) of the product-equivalence piEquivPiSubtypeProd is measurable.

Русский

Обратная (симметрическая) к произведению-эквивалентности piEquivPiSubtypeProd измерима.

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem measurable_piCongrLeft (f : δ' ≃ δ) : Measurable (Equiv.piCongrLeft X f) :=
  by
  rw [measurable_pi_iff]
  intro i
  simp_rw [Equiv.piCongrLeft_apply_eq_cast]
  exact Measurable.eq_mp X (f.apply_symm_apply i) <| measurable_pi_apply <| f.symm i

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