MeasurableSpace.comap API

Stream: Is there code for X?

[Terence Tao]

Is there a reason why the following basic property of docs#MeasurableSpace.comap does not currently appear to be in the API?

import Mathlib

example {α : Type u_1} {β : Type u_2} (m : MeasurableSpace β) (f : α → β) (t : Set α) :
  @MeasurableSet α (MeasurableSpace.comap f m) t ↔ ∃ (s : Set β), MeasurableSet s ∧ f ⁻¹' s = t := by
  rfl

I struggled for some time to prove this fact from the given API until, in desperation, I finally looked at the source code for the definition for MeasurableSpace.comap and found that what I wanted was in fact part of the definition. But I think it would make sense to make this an explicit API method. (There is docs#MeasurableSpace.comap_eq_generateFrom, but this does not easily imply the above statement due to the insertion of MeasurableSpace.generateFrom.)

[Sébastien Gouëzel]

Yes, we should definitely have this as a lemma. Since it's rfl, it's probably possible to work around it most of the time, but still it should be there as a standalone lemma.

[Terence Tao]

A related trivial lemma that also seems to be missing from the API:

example {Ω: Type*} (hΩ hΩ': MeasurableSpace Ω) (h: hΩ ≤ hΩ') {E: Set Ω} (hE: @MeasurableSet Ω hΩ E) : @MeasurableSet Ω hΩ' E := h E hE