∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X] (Y : Type u_2) [inst_1 : MeasurableSpace Y]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [BorelSpace X] [BorelSpace Y]
  [SecondCountableTopologyEither X Y], BorelSpace (WithLp p (X × Y))