fact: Definition conv_fun_seq := {f' : CSetoid_fun (subset (Compact Hab)) IR | {contf' : Continuous_I Hab (PartInt f') | conv_fun_seq' a b Hab f (PartInt f') contf contf'}}.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval