proposition: Lemma LocatedSubset_union : forall (X : MetricSpace) (Y Z : X -> Prop), LocatedSubset X Y -> LocatedSubset X Z -> LocatedSubset X (fun x => Y x \/ Z x).
proof: Proof. intros X Y Z Yloc Zloc d e x ltde. destruct (Yloc d e x ltde) as [farY|closeY]. - destruct (Zloc d e x ltde) as [farZ|closeZ]. left. intros y [H|H]. apply farY, H. apply farZ, H. right. destruct closeZ as [y closeZ]. exists y. split. right. apply closeZ. apply closeZ. - right. destruct closeY as [y closeY]. exists y. split. left. apply closeY. apply closeY. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact