proposition: Lemma hausdorffBall_wd :forall (e1 e2:Q), (e1 == e2) -> forall A1 A2, (forall x, A1 x <-> A2 x) -> forall B1 B2, (forall x, B1 x <-> B2 x) -> (hausdorffBall e1 A1 B1 <-> hausdorffBall e2 A2 B2).
proof: Proof. intros. unfold hausdorffBall. setoid_replace (hemiMetric e1 A1 B1) with (hemiMetric e2 A2 B2). setoid_replace (hemiMetric e1 B1 A1) with (hemiMetric e2 B2 A2). 2: apply hemiMetric_wd; auto. 2: apply hemiMetric_wd; auto. rewrite H. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.logic.Classic CoRN.metric2.Metric CoRN.metric2.Classification Coq.Lists.List Coq.ZArith.ZArith CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax