proposition: Lemma cont_fun_th1 (f: fterm) b: b <o aleph1 -> ord_below_b f b -> exists (F: fterm2), [/\ forall i x, i <o omega0 -> x <o b -> ordinalp (F i x), forall i, i <o omega0 -> ocontinuous_below (fun x => F i x) b & forall x, x <o b -> olimit (fun i => (F i x)) omega0 (f x)].
proof: Proof. move: OS_omega => oo ha hb. have ob := (proj31_1 ha). case: (ozero_dichot ob) => bp. rewrite bp;exists (fun i j => \0o); split. - by move => i j iN /olt0. - by move => i io j _ /olt0. - by move => i /olt0. have neb: nonempty b by move/(oltP ob): bp => h; ex_tac. have [_ /countableP ]: countable_ordinal b. by apply /aleph_oneP; rewrite - Cantor_omega_pr3; apply/(oltP (proj32_1 ha)). rewrite aleph0_pr1 => la. move:(card_le_surj la neb) => [g [bg sg tg]]. have fg: function g by fct_tac. pose Ei i := fun_image (csucc i) (Vf g). have Ei_lim x: x <o b -> exists2 n, natp n & forall i, natp i -> n <=c i -> inc x (Ei i). move/(oltP ob); rewrite -tg => /(proj2 bg); rewrite sg. by move => [n nN ->]; exists n => // i iN lin; apply: funI_i; apply/NleP. pose Bi i x := Zo (Ei i) (fun v => x <=o v). pose F i x := f (intersection (Bi i x)). have ra i x: Bi i x = emptyset -> F i x = f \0o. by rewrite /F; move ->; rewrite setI_0. have rb i x: Bi i x = emptyset -> ordinalp (F i x). by move => /ra ->; apply: hb. have rc i x: natp i -> ordinal_set (Bi i x). by move => iN z /Zo_hi/proj32. have rd i x: i <o omega0 -> ordinalp (F i x). move => /(oltP oo) iN; case: (emptyset_dichot (Bi i x)); first by apply: rb. move => ne; move: (ordinal_setI ne (rc _ _ iN)) => /Zo_S /funI_P[j ja jb]. rewrite /F jb; apply: hb; apply/(oltP ob); Wtac; rewrite sg. move/(NleP iN): ja => lji; apply: (NS_le_nat lji iN). have rdbis i x: i <o omega0 -> x <o b -> ordinalp (F i x) by fprops. have rf x: x <o b -> olimit (fun i => F i x) omega0 (f x). move => lxb. move/(oltP ob): (lxb) => ixb. apply: olimit_econst; first by apply: hb. move:(Ei_lim x lxb) =>[n nN np]. exists n; first by apply/(oltP oo). move => i lni lio. have iN: natp i by apply/(oltP oo). have clni: n <=c i by apply:(ocle3 (CS_nat nN) (CS_nat iN) lni). move:(np _ iN clni) => xE. have xB: inc x (Bi i x) by apply:(Zo_i xE); apply: (oleR (proj31_1 lxb)). have ne: nonempty (Bi i x) by ex_tac. move:(least_ordinal0 (rc i x iN) ne) =>[sa /Zo_hi sb sc]. by rewrite /F (oleA (sc _ xB) sb). exists F; split => // i lio x lx lxb. move/(oltP ob): (lxb) => ixb; move/(oltP oo): (lio) => iN. rewrite /ocontinuous_at /F; apply: olimit_econst; first by apply:rd. pose Ci := (Ei i) -s (Bi i x). case: (emptyset_dichot Ci) => Cie. exists \0o;[ by apply: limit_pos | move => y _ lyx]. have eq1: (Bi i x) = Ei i. apply: extensionality; [apply:Zo_S | apply: (empty_setC Cie)]. have eq2: (Bi i y)= (Bi i x). rewrite eq1; apply: extensionality; first by apply: Zo_S. move => v ve; apply: (Zo_i ve). by move: ve; rewrite - eq1 => /Zo_hi => lxv; apply:(oleT (proj1 lyx) lxv). by rewrite eq2. have cip a: inc a Ci -> inc a (Ei i) /\ a <o x. move => /setC_P [ae etc]; split => //. move/funI_P: (ae) => [z /(NleP iN) lzi eq1]. have lab : a <o b. by apply/(oltP ob); rewrite eq1; Wtac; rewrite sg; apply: (NS_le_nat lzi iN). case: (oleT_el (proj31_1 lxb) (proj31_1 lab)) => // lxa. by case: etc; apply:Zo_i. have [a aCi amaxCi]: exists2 a, inc a Ci & forall z, inc z Ci -> z <=o a. have: ordinal_set Ci by move => t /cip/proj2/proj31_1. have: sub Ci (fun_image (csucc i) (Vf g)). by move => t /setC_P []. clear cip;move: iN Ci Cie; clear; move: i; apply: Nat_induction. move => A [t tA] ap osA; exists t => // z zA. rewrite succ_zero in ap. move:(oleR (osA _ tA)). move: (ap _ tA) => /funI_P [u /set1_P -> ->]. by move: (ap _ zA) => /funI_P [uu /set1_P -> ->]. move => n nN Hrec C neC sC osc. set w := (Vf g (csucc n)). have sN := (NS_succ nN). have: sub (C -s1 w) (fun_image (csucc n) (Vf g)). move => t /setC1_P [/sC /funI_P [z /(NleP sN) lt ->] tw]. case:(cle_eqVlt lt); [ by move => h; case: tw; ue | move/(NltP sN) => le ]. by apply: funI_i. case: (inc_or_not w C) => wC; last first. by rewrite (setC1_eq wC) => ssC; apply: Hrec. have ow: ordinalp w by apply: osc. move => ss1; case: (emptyset_dichot (C -s1 w)) => c1E. exists w => // z zC; case: (equal_or_not z w) => ezw. by rewrite ezw; apply: oleR. by empty_tac1 z; apply/setC1_P. have os1: ordinal_set (C -s1 w) by move => t/setC1_P/proj1/osc. move: (Hrec _ c1E ss1 os1) => [a ac ap]. exists (omax a w). by rewrite/omax /Gmax;Ytac h => //; case/ setC1_P: ac. move: (omax_p1 (os1 _ ac) ow) => [qa qb]. move => z zc; case: (equal_or_not z w) => ezw; first by rewrite ezw. by apply: oleT qa; apply: ap; apply/setC1_P. move:(cip _ aCi) => [aE lax]; exists (osucc a). by move/limit_ordinal_P: lx =>[ _ h]; apply: h. move => y /oleSltP lay lyx. suff eq2: (Bi i x) = (Bi i y) by rewrite - eq2. set_extens t => /Zo_P [yEi cp]; apply:(Zo_i yEi). exact:(oleT (proj1 lyx) cp). case: (inc_or_not t (Bi i x)); first by move/Zo_hi. move => tnbi. have: inc t Ci by apply/setC_P. by move/amaxCi => ta; case:(oleNgt (oleT cp ta)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)