class QuasiBorelSpace.SeparatesPoints (A : Type u_5) [QuasiBorelSpace A] : Prop

A QuasiBorelSpace separates points if any two elements are equal iff all morphism predicates agree on the elements.

This class is the QuasiBorelSpace analogue of MeasurableSingletonClass.

• separates (x y : A) : (∀ (p : A → Prop), IsHom p → p x → p y) → x = y

  Two elements are equal iff they agree for all morphism predicates.

theorem QuasiBorelSpace.separatesPoints_def {A : Type u_1} [QuasiBorelSpace A] [SeparatesPoints A] {x y : A} (h : ∀ (p : A → Prop), IsHom p → p x → p y) : x = y

instance QuasiBorelSpace.instSeparatesPointsOfDiscreteQuasiBorelSpace {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [DiscreteQuasiBorelSpace A] : SeparatesPoints A

instance QuasiBorelSpace.instSeparatesPointsProd {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [SeparatesPoints A] [SeparatesPoints B] : SeparatesPoints (A × B)

instance QuasiBorelSpace.instSeparatesPointsForall {I : Type u_3} {P : I → Type u_4} [(i : I) → QuasiBorelSpace (P i)] [∀ (i : I), SeparatesPoints (P i)] : SeparatesPoints ((i : I) → P i)

instance QuasiBorelSpace.instSeparatesPointsSigma {I : Type u_3} [Countable I] {P : I → Type u_4} [(i : I) → QuasiBorelSpace (P i)] [∀ (i : I), SeparatesPoints (P i)] : SeparatesPoints ((i : I) × P i)

instance QuasiBorelSpace.instSeparatesPointsSum {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [SeparatesPoints A] [SeparatesPoints B] : SeparatesPoints (A ⊕ B)

instance QuasiBorelSpace.instSeparatesPointsQuasiBorelHom {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [SeparatesPoints A] [SeparatesPoints B] : SeparatesPoints (A →𝒒 B)

instance QuasiBorelSpace.instSeparatesPointsOfSeparatesPointsOfMeasurableQuasiBorelSpace {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [MeasurableSpace.SeparatesPoints A] [MeasurableQuasiBorelSpace A] : SeparatesPoints A