proposition: Lemma regFun_is_MetricSpace : is_MetricSpace (@regFunBall _ (@ball X)).
proof: Proof. unfold regFunBall. split. - intros e epos f d1 d2. rewrite <- Qplus_assoc, (Qplus_comm e), Qplus_assoc. apply ball_weak. exact epos. apply regFun_prf. - intros e f g H d1 d2. apply ball_sym. rewrite Qplus_comm, <- (Qplus_comm e), Qplus_assoc. apply H. - intros e1 e2 a b c Hab Hbc d1 d2. apply ball_closed. intros d3 dpos. setoid_replace (proj1_sig d1+(e1+e2)+proj1_sig d2+d3) with ((proj1_sig d1 + e1 + (1#2)*d3)+((1#2)*d3 + e2 + proj1_sig d2)) by (simpl; ring). eapply ball_triangle. apply (Hab d1 ((1#2)*exist _ _ dpos)%Qpos). apply (Hbc ((1#2)*exist _ _ dpos)%Qpos). - intros e a b H d1 d2. apply ball_closed. intros d dpos. setoid_replace (proj1_sig d1+e+ proj1_sig d2+d) with (proj1_sig d1 + (e+d) + proj1_sig d2) by (simpl; ring). apply H, dpos. - intros. apply Qnot_lt_le. intro abs. assert (0 < -e * (1#3)). { apply (Qmult_lt_l _ _ (3#1)). reflexivity. apply (Qplus_lt_l _ _ e). ring_simplify. apply (Qlt_le_trans _ _ _ abs). discriminate. } specialize (H (exist _ _ H0) (exist _ _ H0)). simpl in H. apply msp_nonneg in H. 2: apply X. ring_simplify in H. apply (Qlt_not_le _ _ abs). apply (Qmult_le_l _ _ (3#9)). reflexivity. rewrite Qmult_0_r. exact H. - intros. apply (msp_stable (msp X)). intro abs. contradict H; intro H. apply abs. apply H. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax