∀ {R : Type u_1} [inst : CommRing R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R]
  (r : ValuativeRel.ValueGroupWithZero R), IsOpen {x | (ValuativeRel.valuation R) x < r}