Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-10 16:50 178e7467

View on Github →

rename towards -> tendsto

Estimated changes

Modified algebra/lattice/filter.lean

added def filter.tendsto

added theorem filter.tendsto_compose

added theorem filter.tendsto_cong

added theorem filter.tendsto_fst

added theorem filter.tendsto_id'

added theorem filter.tendsto_id

added theorem filter.tendsto_inf

added theorem filter.tendsto_map'

added theorem filter.tendsto_map

added theorem filter.tendsto_prod_mk

added theorem filter.tendsto_snd

added theorem filter.tendsto_vmap''

added theorem filter.tendsto_vmap'

added theorem filter.tendsto_vmap

deleted def filter.towards

deleted theorem filter.towards_compose

deleted theorem filter.towards_cong

deleted theorem filter.towards_fst

deleted theorem filter.towards_id'

deleted theorem filter.towards_id

deleted theorem filter.towards_inf

deleted theorem filter.towards_map'

deleted theorem filter.towards_map

deleted theorem filter.towards_prod_mk

deleted theorem filter.towards_snd

deleted theorem filter.towards_vmap''

deleted theorem filter.towards_vmap'

deleted theorem filter.towards_vmap

Modified topology/continuity.lean

added theorem continuous_iff_tendsto

deleted theorem continuous_iff_towards

added theorem dense_embedding.tendsto_ext

deleted theorem dense_embedding.towards_ext

added theorem tendsto_nhds_iff_of_embedding

deleted theorem towards_nhds_iff_of_embedding

Modified topology/real.lean

modified theorem lift_rat_fun_of_rat

modified theorem of_rat_add

modified theorem of_rat_inv

modified theorem of_rat_mul

modified theorem of_rat_neg

modified theorem of_rat_one

modified theorem of_rat_sub

modified theorem of_rat_zero

added theorem tendsto_add_rat

added theorem tendsto_add_rat_zero'

added theorem tendsto_add_rat_zero

added theorem tendsto_inv_pos_rat

added theorem tendsto_inv_rat

added theorem tendsto_inv_real

added theorem tendsto_mul_bnd_rat'

added theorem tendsto_mul_bnd_rat

added theorem tendsto_mul_rat'

added theorem tendsto_mul_rat

added theorem tendsto_neg_rat

added theorem tendsto_neg_rat_zero

added theorem tendsto_of_uniform_continuous_subtype

added theorem tendsto_sub_rat'

added theorem tendsto_sub_uniformity_zero_nhd'

added theorem tendsto_sub_uniformity_zero_nhd

added theorem tendsto_zero_nhds

deleted theorem towards_add_rat

deleted theorem towards_add_rat_zero'

deleted theorem towards_add_rat_zero

deleted theorem towards_inv_pos_rat

deleted theorem towards_inv_rat

deleted theorem towards_inv_real

deleted theorem towards_mul_bnd_rat'

deleted theorem towards_mul_bnd_rat

deleted theorem towards_mul_rat'

deleted theorem towards_mul_rat

deleted theorem towards_neg_rat

deleted theorem towards_neg_rat_zero

deleted theorem towards_of_uniform_continuous_subtype

deleted theorem towards_sub_rat'

deleted theorem towards_sub_uniformity_zero_nhd'

deleted theorem towards_sub_uniformity_zero_nhd

deleted theorem towards_zero_nhds

Modified topology/topological_space.lean

added theorem tendsto_const_nhds

added theorem tendsto_nhds

added theorem tendsto_nhds_unique

deleted theorem towards_const_nhds

deleted theorem towards_nhds

deleted theorem towards_nhds_unique

Modified topology/uniform_space.lean

added theorem tendsto_const_uniformity

added theorem tendsto_left_nhds_uniformity

added theorem tendsto_prod_uniformity_fst

added theorem tendsto_prod_uniformity_snd

added theorem tendsto_right_nhds_uniformity

added theorem tendsto_swap_uniformity

deleted theorem towards_const_uniformity

deleted theorem towards_left_nhds_uniformity

deleted theorem towards_prod_uniformity_fst

deleted theorem towards_prod_uniformity_snd

deleted theorem towards_right_nhds_uniformity

deleted theorem towards_swap_uniformity