prod_le_borel_prod

Stream: mathlib4

[Kevin Buzzard]

docs#prod_le_borel_prod is a bit strange because it only applies to borel, as opposed to an arbitrary [m : MeasurableSpace (α × β)] [BorelSpace (α × β)]. How about this for a variant:

theorem prod_le_measurableSpace_of_borelSpace {α β : Type*}
    [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
    [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β]
    [m : MeasurableSpace (α × β)] [BorelSpace (α × β)] :
    Prod.instMeasurableSpace ≤ m := by
  simpa [BorelSpace.measurable_eq (α := α × β)] using prod_le_borel_prod

I find myself wanting this one in FLT rather than prod_le_borel_prod, becasue I am putting [MeasurableSpace X] [BorelSpace X] assumptions on topological spaces when these are necessary to make theorem statements about Haar characters compile. Would this lemma be welcome in mathlib? I still don't really know much about the measurable space part of the library. Is it already there?

[Yury G. Kudryashov]

I don't like the idea of having conflicting instances.

[Kevin Buzzard]

Oh! I had not spotted that Prod.instMeasurableSpace was an instance! But I don't want this measurable space structure on my product, I want the Borel space structure.

[Kevin Buzzard]

Although everything is second countable or whatever in my application, so they will actually be equal. Hmm.

[Yury G. Kudryashov]

I see 2 options:

• if you care about spaces that aren't second countable and you have enough theorems that assume inst \le borel _, then we can add a typeclass claiming this inequality; then we can see what can be generalized from BorelSpace to this assumption;
• if not, then you can add SecondCountableTopology as assumptions and use the BorelSpace instance for Prod.