proposition: Lemma CVU_cont_open (fn : nat -> R -> R) (D : R -> Prop) : open D -> CVU_dom fn D -> (forall n, forall x, D x -> continuity_pt (fn n) x) -> forall x, D x -> continuity_pt (fun y => real (Lim_seq (fun n => fn n y))) x.
proof: Proof. move => Ho Hfn Hc x Hx. case: (fun H => CVU_limits_open fn D Ho Hfn H x Hx) => [{Hx} x n Hx | Hex_s [Hex_f Heq]]. exists (fn n x). apply is_lim_spec. intros eps. case: (Hc n x Hx eps (cond_pos eps)) => {Hc} d [Hd Hc]. exists (mkposreal d Hd) => /= y Hy Hxy. apply (Hc y). split. split. exact: I. by apply sym_not_eq, Hxy. exact: Hy. apply Lim_correct' in Hex_f. rewrite -Heq in Hex_f => {Heq}. replace (Lim_seq (fun n : nat => real (Lim (fn n) x))) with (Lim_seq (fun n : nat => (fn n) x)) in Hex_f. move => e He. apply is_lim_spec in Hex_f. case: (Hex_f (mkposreal e He)) => {Hex_f} /= delta Hex_f. exists delta ; split => [ | y [[_ Hxy] Hy]]. by apply delta. apply Hex_f. exact: Hy. by apply sym_not_eq. apply Lim_seq_ext => n. replace (fn n x) with (real (fn n x)) by auto. apply sym_eq, f_equal, is_lim_unique. apply is_lim_spec. move => eps. case: (Hc n x Hx eps (cond_pos eps)) => {Hc} d [Hd Hc]. exists (mkposreal d Hd) => /= y Hy Hxy. apply (Hc y). split. split. exact: I. by apply sym_not_eq, Hxy. exact: Hy. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Continuity Derive Series Lub Hierarchy