∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : CommSemiring R] {A : Type u_3}
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : IsTopologicalSemiring A],
  Monotone fun s => s.SeparatesPoints