proposition: Lemma cont_fun_th4 (f: fterm2) bi bx (g := fun x => \osup (fun_image bi (fun i => f i x))): limit_ordinal bi -> ordinalp bx -> (forall i j x, i <=o j -> j <o bi -> x <o bx -> f i x <=o f j x) -> (forall i x y, i <o bi -> x <=o y -> y <o bx -> f i x <=o f i y) -> (forall i, i <o bi -> ocontinuous_below (f i) bx) -> ocontinuous_below g bx.
proof: Proof. move => lbi obx ha hb hc. move:(cont_fun_th4_aux lbi obx ha hb) =>[he hf hg hh]. move => x xlim lxb; split. by exists \0o; [ apply: limit_pos | move => u _ /proj1 ux; apply: hg]. move => l llg. move:(olt_sup (he _ lxb)llg) => [v /funI_P [z /(oltP (proj31 lbi)) zl ->]] lt2. move:(proj2 (hc _ zl x xlim lxb) _ lt2) =>[y ya yb]; exists y => // t ta tb. exact: (olt_leT (yb t ta tb) (hh _ _ zl (olt_ltT tb lxb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)