equal
deleted
inserted
replaced
299 LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff |
299 LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff |
300 LIMSEQ_imp_rabs ~> tendsto_rabs |
300 LIMSEQ_imp_rabs ~> tendsto_rabs |
301 LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] |
301 LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] |
302 LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] |
302 LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] |
303 LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] |
303 LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] |
|
304 LIMSEQ_Complex ~> tendsto_Complex |
304 LIM_ident ~> tendsto_ident_at |
305 LIM_ident ~> tendsto_ident_at |
305 LIM_const ~> tendsto_const |
306 LIM_const ~> tendsto_const |
306 LIM_add ~> tendsto_add |
307 LIM_add ~> tendsto_add |
307 LIM_add_zero ~> tendsto_add_zero |
308 LIM_add_zero ~> tendsto_add_zero |
308 LIM_minus ~> tendsto_minus |
309 LIM_minus ~> tendsto_minus |