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