|
/top,prelude_aux,prelude_A4,appendix,prelude_sqrt,cauchy,int,add,neg,sub,mul,inv,unique,div,rat,shift,min,max,sqrtx,bisection_nat_sqrt,power,sum,series,powerseries,atanx,asinx,acosx,sincosx,remx,trigx,log,exp,hyperbolicx,test
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,poly_rew,sign,log_nat,sqrt_exists,root,polynomials,prelude_aux,harmonic_polynomials,real_fun_ops,sigma_below,intervals_real,quadratic,real_fun_props,sigma_upto,sigma_swap,real_facts,exponent_props,product,factorial_props,sigma,sqrt,sq,sigma_nat
trig_fnd/trig_values,atan_approx,sincos_def,trig_ineq,trig_approx,acos,exp_term,sincos_phase,atan2,asin,trig_extra,trig_basic,tan_quad,sincos_quad,atan,sincos
series/power_series_derivseq,series,power_series,power_series_deriv,taylor_series,power_series_integ,power_series_conv,power_series_deriv_scaf
lnexp_fnd/hyperbolic,expt,ln_exp,ln_series,ln_exp_series_alt,convergence_special,ln_approx
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,taylors,integral_split_scaf,restrict2_deriv,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,derivatives_def,partitions_scaf,continuous_functions_more,integral_step,real_fun_supinf,sequence_props,chain_rule,integral_bounded,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:prelude_aux,prelude_A4,appendix,prelude_sqrt,cauchy,int,add,neg,sub,mul,inv,div,rat,shift,min,max,sqrtx,power,sum,series,powerseries,atanx,asinx,acosx,sincosx,trigx,log,exp,hyperbolicx,test
prelude_aux:reals@sqrt,lnexp_fnd@ln_exp
prelude_A4:prelude_aux,reals@sqrt
appendix:prelude_aux,prelude_A4,reals@sqrt
prelude_sqrt:prelude_aux
cauchy:prelude_aux,appendix
int:cauchy
add:appendix,cauchy
neg:cauchy
sub:add,neg
mul:prelude_aux,appendix,cauchy
inv:prelude_aux,appendix,cauchy,unique,neg
unique:prelude_aux,cauchy,neg,add
div:mul,inv
rat:cauchy,int,div
shift:prelude_aux,appendix,cauchy
min:cauchy
max:cauchy
sqrtx:prelude_aux,appendix,cauchy,unique,reals@sqrt,bisection_nat_sqrt
bisection_nat_sqrt:appendix
power:prelude_aux,prelude_A4,appendix,cauchy,unique
sum:prelude_aux,prelude_A4,appendix,cauchy,unique,power,reals@sigma
series:prelude_aux
powerseries:prelude_aux,appendix,cauchy,mul,power,sum
atanx:prelude_aux,sqrtx,int,add,sub,mul,div,shift,cauchy,sum,power,powerseries,trig_fnd@atan
asinx:atanx,trig_fnd@asin
acosx:asinx,trig_fnd@acos
sincosx:prelude_aux,atanx,trig_fnd@sincos,trig_fnd@trig_values,reals@factorial_props,trig_fnd@trig_approx,remx
remx:
trigx:sincosx
log:prelude_aux,cauchy,add,sub,neg,int,inv,mul,div,shift,sqrtx,powerseries,lnexp_fnd@ln_exp,lnexp_fnd@ln_exp_series_alt
exp:prelude_aux,cauchy,inv,int,shift,powerseries,log,reals@factorial,lnexp_fnd@ln_exp,lnexp_fnd@ln_exp_series_alt,lnexp_fnd@ln_approx
hyperbolicx:lnexp_fnd@hyperbolic,log,exp
test:trigx,hyperbolicx
[ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
]
|
