equal
deleted
inserted
replaced
294 LIMSEQ_setsum ~> tendsto_setsum |
294 LIMSEQ_setsum ~> tendsto_setsum |
295 LIMSEQ_setprod ~> tendsto_setprod |
295 LIMSEQ_setprod ~> tendsto_setprod |
296 LIMSEQ_norm_zero ~> tendsto_norm_zero_iff |
296 LIMSEQ_norm_zero ~> tendsto_norm_zero_iff |
297 LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff |
297 LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff |
298 LIMSEQ_imp_rabs ~> tendsto_rabs |
298 LIMSEQ_imp_rabs ~> tendsto_rabs |
|
299 LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] |
|
300 LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] |
|
301 LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] |
299 LIM_ident ~> tendsto_ident_at |
302 LIM_ident ~> tendsto_ident_at |
300 LIM_const ~> tendsto_const |
303 LIM_const ~> tendsto_const |
301 LIM_add ~> tendsto_add |
304 LIM_add ~> tendsto_add |
302 LIM_add_zero ~> tendsto_add_zero |
305 LIM_add_zero ~> tendsto_add_zero |
303 LIM_minus ~> tendsto_minus |
306 LIM_minus ~> tendsto_minus |