proposition: Lemma Eball_spec ε (x y : X) : ball ε x y ↔ ball ε (f x) (f y).
proof: Proof. intuition. Qed.
imports: CoRN.metric2.Metric CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid CoRN.stdlib_omissions.Q CoRN.model.totalorder.QMinMax CoRN.metric2.Complete CoRN.metric2.Prelength MathClasses.interfaces.abstract_algebra