proposition: Lemma preserves_unary_fun x : F (Cmap plX g x) = Cmap plY h (F x).
proof: Proof. intros e1 e2. apply regFunEq_equiv. apply regFunEq_e. intros ε. simpl. rewrite QposInf_bind_id. apply (ball_wd _ eq_refl _ _ (g_eq_h _) _ _ (reflexivity _)). 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