proposition: Lemma preserves_unary_complete_fun x : F (Cbind plX g x) = Cbind plY h (F x).
proof: Proof. pose (exist (Qlt 0) (1#2) eq_refl) as half. intros ? ?. rewrite Qplus_0_r. apply regFunEq_e. intros ε. simpl. unfold Cjoin_raw. simpl. rewrite QposInf_bind_id. apply ball_weak. apply Qpos_nonneg. assert (QposEq ε (half * ε + half * ε)) by (unfold QposEq; simpl; ring). apply (ball_wd _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. pose proof (g_eq_h (approximate x (mu h (half * ε)))). apply regFunEq_equiv in H0. apply H0. 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