measurable set of quotient image?

Stream: Is there code for X?

[Alex Kontorovich]

Do we have something like the measurability of the forward image of a quotient map? (Do I need some more assumptions perhaps?) We have measurableSet_quotient which deals with preimages...

import Mathlib.MeasureTheory.Group.Action

variable {G : Type*} {α : Type*} [Group G] [MulAction G α] [MeasurableSpace α]

local notation "π" => @Quotient.mk _ (MulAction.orbitRel G α)

example [Countable G] [MeasurableSpace G] [inst_6 : MeasurableSMul G α] (S : Set α)
    (hS : MeasurableSet S) : MeasurableSet (π '' S) := by
  sorry

Thanks!

[Anatole Dedecker]

I don't know wether we have it, but here is a proof:

import Mathlib.MeasureTheory.Group.Action
import Mathlib.MeasureTheory.Group.Pointwise

variable {G : Type*} {α : Type*} [Group G] [MulAction G α] [MeasurableSpace α]

local notation "π" => Quotient.mk (MulAction.orbitRel G α)

example [Countable G] [MeasurableSpace G] [MeasurableSMul G α] (S : Set α)
    (hS : MeasurableSet S) : MeasurableSet (π '' S) := by
  let _ : Setoid α := MulAction.orbitRel G α
  rw [measurableSet_quotient, Quotient.mk''_eq_mk, ← Quotient.mk'_eq_mk,
      MulAction.quotient_preimage_image_eq_union_mul]
  exact .iUnion fun g ↦ hS.const_smul _

[Alex Kontorovich]

Ah thanks, so I should be doing all these conversions between Quotient.mk, Quotient.mk', and Quotient.mk''... May I ask why we have the three...?

[Yury G. Kudryashov]

Because nobody cleaned it up after migration.

[Ruben Van de Velde]

I started looking at removing one of them but got distracted. I may try to find the code later