Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-05 14:15 581cf19b

View on Github →

feat(topology): split uniform_space and topological_structure

Estimated changes

added theorem continuous_inv'
added theorem continuous_inv
added theorem continuous_sub'
added theorem continuous_sub
added theorem exists_nhds_split4
added theorem exists_nhds_split
added theorem exists_nhds_split_inv
added theorem is_open_map_mul_left
added theorem is_open_map_mul_right
added theorem nhds_one_symm
added theorem nhds_translation
added theorem tendsto_inv
added theorem tendsto_sub
deleted theorem to_uniform_space_eq
added theorem continuous_finset_prod
added theorem continuous_list_prod
added theorem continuous_mul'
added theorem continuous_mul
added theorem continuous_pow
added theorem tendsto_finset_prod
added theorem tendsto_list_prod
added theorem tendsto_mul'
added theorem tendsto_mul
added theorem tendsto_multiset_prod
deleted theorem continuous_finset_prod
deleted theorem continuous_inv'
deleted theorem continuous_inv
deleted theorem continuous_list_prod
deleted theorem continuous_mul'
deleted theorem continuous_mul
deleted theorem continuous_multiset_prod
deleted theorem continuous_pow
deleted theorem continuous_sub'
deleted theorem continuous_sub
deleted theorem exists_nhds_split4
deleted theorem exists_nhds_split
deleted theorem exists_nhds_split_inv
deleted theorem group_separation_rel
deleted def ideal.closure
deleted theorem ideal.coe_closure
deleted theorem is_open_map_mul_left
deleted theorem is_open_map_mul_right
deleted theorem nhds_one_symm
deleted theorem nhds_translation
deleted theorem nhds_translation_mul_inv
deleted theorem tendsto_finset_prod
deleted theorem tendsto_inv
deleted theorem tendsto_list_prod
deleted theorem tendsto_mul'
deleted theorem tendsto_mul
deleted theorem tendsto_multiset_prod
deleted theorem tendsto_sub
deleted theorem uniform_add_group.mk'
deleted theorem uniform_continuous_add'
deleted theorem uniform_continuous_add
deleted theorem uniform_continuous_neg'
deleted theorem uniform_continuous_neg
deleted theorem uniform_continuous_sub'
deleted theorem uniform_continuous_sub
deleted theorem uniformity_translate
deleted def cauchy
deleted theorem cauchy_comap
deleted theorem cauchy_downwards
deleted theorem cauchy_iff
deleted theorem cauchy_iff_exists_le_nhds
deleted theorem cauchy_map
deleted theorem cauchy_map_iff
deleted theorem cauchy_nhds
deleted theorem cauchy_prod
deleted theorem cauchy_pure
deleted def cauchy_seq
deleted theorem cauchy_seq_iff_prod_map
deleted theorem complete_space_extension
deleted theorem complete_univ
deleted theorem is_closed_of_is_complete
deleted def is_complete
deleted theorem is_complete_image_iff
deleted theorem is_complete_of_is_closed
deleted theorem le_nhds_lim_of_cauchy
deleted theorem le_nhds_of_cauchy_adhp
deleted def separated
deleted theorem separated_def'
deleted theorem separated_def
deleted theorem separated_equiv
deleted def totally_bounded
deleted theorem totally_bounded_closure
deleted theorem totally_bounded_empty
deleted theorem totally_bounded_image
deleted theorem totally_bounded_preimage
deleted theorem totally_bounded_subset
deleted theorem uniform_embedding.prod
deleted def uniform_embedding
deleted theorem uniform_embedding_comap
deleted theorem uniform_embedding_def'
deleted theorem uniform_embedding_def
deleted theorem uniform_extend_subtype
deleted theorem uniformly_extend_exists
deleted theorem uniformly_extend_of_emb
deleted theorem uniformly_extend_spec
deleted theorem tendsto_sub_comap_self