proposition: Lemma LocatedSubset_stable : forall (X : MetricSpace) (Y : X -> Prop), LocatedSubset X Y -> LocatedSubset X (fun x => ~~Y x).
proof: Proof. intros. intros d e x dlte. specialize (X0 d e x dlte) as [far|close]. - left. intros y H abs. contradict H; intro H. revert abs. apply far, H. - right. destruct close as [y close]. exists y. split. intro abs. destruct close; contradiction. apply close. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact