Points of a quotient measurable space

For an equivalence relation E on a measurable space X, a singleton {⟦x⟧} of Quotient E is measurable for Mathlib's quotient σ-algebra exactly when its preimage, the class of x, is measurable in X. So if every class of E is measurable, the quotient has measurable singletons, and if there are moreover countably many classes, Mathlib's instance MeasurableSingletonClass.toDiscreteMeasurableSpace makes every subset of the quotient measurable.

Main results

• Setoid.measurableSingletonClass_quotient: measurable classes give measurable singletons.

theorem Setoid.measurableSingletonClass_quotient {X : Type u_1} [MeasurableSpace X] {E : Setoid X} (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : MeasurableSingletonClass (Quotient E)

If every class of E is measurable, then the quotient σ-algebra on Quotient E has measurable singletons.