proposition: Lemma Continuous_power : positive_fun J F -> Continuous J F -> Continuous J G -> Continuous J FPower.
proof: Proof. intros H H0 H1. unfold FPower in |- *. apply Continuous_comp with realline. 3: apply Continuous_Exp. 2: apply Continuous_mult; [ apply H1 | apply Continuous_comp with (openl [0]); auto ]. 3: apply Continuous_Log. apply maps_compacts_into_strict_imp_weak; apply Continuous_imp_maps_compacts_into. apply Continuous_mult; auto. apply Continuous_comp with (openl [0]); auto. 2: apply Continuous_Log. apply maps_compacts_into_strict_imp_weak; apply positive_imp_maps_compacts_into; auto. apply maps_compacts_into_strict_imp_weak; apply positive_imp_maps_compacts_into; auto. Qed.
imports: CoRN.transc.Exponential