proposition: Lemma preserves_binary_fun x y : F (Cmap2 plX plX g x y) = Cmap2 plY plY h (F x) (F y).
proof: Proof. intros e1 e2. apply regFunEq_equiv, regFunEq_e. intros ε. simpl. unfold Cap_raw. simpl. apply (ball_wd _ eq_refl _ _ (g_eq_h _ _) _ _ (reflexivity _)). rewrite 2!QposInf_bind_id. apply ball_refl. apply (Qpos_nonneg (ε + ε)). 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