proposition: Lemma continuity_pt_recip_interv : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub), (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) -> (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) -> (forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) -> (forall a, lb <= a <= ub -> continuity_pt f a) -> forall b, f lb < b < f ub -> continuity_pt g b.
proof: Proof. intros f g lb ub lb_lt_ub f_incr_interv f_eq_g g_wf. assert (g_eq_f_prelim := leftinv_is_rightinv_interv f g lb ub f_incr_interv f_eq_g). assert (g_eq_f : forall x, lb <= x <= ub -> (comp g f) x = id x). { intro x ; apply g_eq_f_prelim ; assumption. } apply (continuity_pt_recip_prelim f g lb ub lb_lt_ub f_incr_interv g_eq_f). Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra