Quelle  lnexp_fnd.dep   Sprache: unbekannt

/top,ln_exp,expt,hyperbolic,exp_series,convergence_special,ln_series,exp_approx,ln_approx,ln_exp_series_alt,ln_exp_ineq
structures/sort_array,permutations,for_iterate,min_array_def,min_seq,sort_seq,max_array_def,below_arrays,seqs,concat_arrays,sort_seq_lems,max_seq,permutations_seq,sort_array_def
reals/real_fun_preds,factorial,binomial,sigma_below_sub,abs_lems,sign,log_nat,sqrt_exists,root,polynomials,prelude_aux,real_fun_ops,sigma_below,intervals_real,quad_minmax,quadratic,real_fun_props,sigma_upto,sigma_swap,real_facts,exponent_props,product,sigma,sqrt,sq,sigma_nat
series/power_series_derivseq,series,power_series,power_series_deriv,taylor_series,power_series_integ,power_series_conv,power_series_deriv_scaf
analysis/step_fun_def,continuous_functions_props,lim_of_functions,derivatives,sqrt_derivative,integral_chg_var,nth_derivatives,deriv_domain,top_sequences,deriv_domains,integral,step_fun_props,continuous_functions,continuity_interval,indefinite_integral,restrict2_deriv,integral_split_scaf,taylors,inverse_continuous_functions,derivative_props,integral_cont_scaf,integral_diff_doms,interval_minmax,integral_cont,step_fun_scaf,unif_cont_fun,fundamental_theorem,monotone_subsequence,convergence_ops,derivative_inverse,convergence_functions,polynomial_deriv,deriv_domain_def,epsilon_lemmas,composition_continuous,integral_split,partitions_scaf,derivatives_def,continuous_functions_more,integral_step,real_fun_supinf,sequence_props,integral_bounded,chain_rule,integral_pulse,integral_def,integral_prep,lim_of_composition,convergence_sequences,continuity_props,derivatives_alt
finite_sets/func_composition,finite_sets_minmax,finite_sets_inductions,finite_sets_card_eq,finite_sets_below
ints/factorial,max_below
top:ln_exp,expt,hyperbolic,exp_series,ln_series,exp_approx,ln_approx,ln_exp_series_alt,ln_exp_ineq
ln_exp:analysis@integral,analysis@indefinite_integral,analysis@chain_rule,analysis@derivative_props,analysis@deriv_domains,analysis@derivative_inverse
expt:ln_exp
hyperbolic:reals@sq,reals@sqrt,analysis@sqrt_derivative,analysis@restrict2_deriv,analysis@deriv_domains,analysis@nth_derivatives,analysis@taylors,analysis@polynomial_deriv,ln_exp,reals@binomial
exp_series:ln_exp,series@taylor_series,ints@factorial,convergence_special,reals@polynomials
convergence_special:expt,ints@factorial,analysis@continuous_functions_more
ln_series:ln_exp,convergence_special,series@taylor_series,analysis@integral_chg_var,reals@abs_lems,analysis@integral_diff_doms,series@power_series_integ
exp_approx:exp_series,reals@quad_minmax
ln_approx:ln_series,reals@log_nat
ln_exp_series_alt:ln_exp,analysis@derivative_inverse,analysis@nth_derivatives,analysis@taylors,series@series,analysis@integral,analysis@indefinite_integral,reals@sqrt
ln_exp_ineq:ln_exp,analysis@derivative_props,analysis@chain_rule,ln_exp_series_alt