proposition: Lemma LocatedSubset_wd : forall (X : MetricSpace) (Y Z : X -> Prop), (forall x:X, Y x <-> Z x) -> LocatedSubset X Y -> LocatedSubset X Z.
proof: Proof. intros X Y Z YeqZ Yloc d e x dlte. destruct (Yloc d e x dlte) as [far|close]. - left. intros y H. apply far, YeqZ, H. - right. destruct close as [y [yin close]]. exists y. split. apply YeqZ, yin. exact close. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact