LeanPool.QuasiBorelSpaces.MeasureTheory.StandardBorelSpace

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.MeasureTheory.StandardBorelSpace.

theorem MeasureTheory.standardBorelSpace_iff (A : Type u_1) [MeasurableSpace A] : StandardBorelSpace A ↔ Countable A ∧ DiscreteMeasurableSpace A ∨ Nonempty (A ≃ᵐ ℝ)