proposition: Lemma Iab_reg_prf : is_RegularFunction (FinEnum_ball AQ_as_MetricSpace) (fun d0:QposInf => match d0 with | Qpos2QposInf d => map (λ x : Q, AppInverse0 x ((1 # 2) * d)%Qpos) (UniformPartition a b (Z.to_pos (Qround.Qceiling ((b - a) / (inject_Z 2 * ((1 # 2) * ` d)))))) | QposInfinity => nil end).
proof: Proof. pose (CompactCompleteCompact _ (CompactImage (1#1)%Qpos plFEQ (Build_UniformlyContinuousFunction inject_Q_AR_uc) (CompactIntervalQ leab))) as K. apply (@is_RegularFunction_wd _ (approximate K)). 2: apply (regFun_prf K). intro d. simpl. unfold Cjoin_raw; simpl. unfold FinCompact_raw; simpl. rewrite map_map; simpl. unfold MetricMorphisms.app_inverse. unfold canonical_names.equiv. unfold FinEnum_eq. simpl. apply (@ball_refl (FinEnum AQ_as_MetricSpace) 0). discriminate. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.metric2.Prelength CoRN.metric2.Compact CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.reals.faster.ARArith CoRN.reals.fast.Interval