fact: Definition LocatedSubset (X : MetricSpace) (Y : X -> Prop) : Type := forall (d e : Q) (x:X), d < e -> { forall y:X, Y y -> ~ball d x y } + { exists y:X, Y y /\ ball e x y }.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact