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

Modified src/algebra/module.lean

Modified src/analysis/exponential.lean

Modified src/analysis/normed_space/operator_norm.lean

Modified src/data/equiv/basic.lean

Modified src/data/quot.lean

Modified src/logic/basic.lean

added theorem {u}

Modified src/topology/algebra/group.lean

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 nhds_translation_mul_inv

added theorem quotient_group.open_coe

added theorem quotient_group_saturate

added theorem tendsto_inv

added theorem tendsto_sub

deleted theorem to_uniform_space_eq

deleted def topological_add_group.to_uniform_space

deleted theorem topological_add_group_is_uniform

deleted theorem uniformity_eq_comap_nhds_zero'

Created src/topology/algebra/group_completion.lean

added theorem coe_zero

added theorem uniform_space.completion.coe_add

added theorem uniform_space.completion.coe_neg

added theorem uniform_space.completion.is_add_group_hom_extension

added theorem uniform_space.completion.is_add_group_hom_map

added theorem uniform_space.completion.is_add_group_hom_prod

Modified src/topology/algebra/infinite_sum.lean

Created src/topology/algebra/monoid.lean

added theorem continuous_finset_prod

added theorem continuous_list_prod

added theorem continuous_mul'

added theorem continuous_mul

added theorem continuous_multiset_prod

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

Renamed src/topology/algebra/topological_structures.lean to src/topology/algebra/ordered.lean

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_of_continuous

deleted theorem uniform_continuous_of_tendsto_zero

deleted theorem uniform_continuous_sub'

deleted theorem uniform_continuous_sub

deleted theorem uniform_embedding_translate

deleted theorem uniformity_eq_comap_nhds_zero

deleted theorem uniformity_translate

Deleted src/topology/algebra/quotient.lean

deleted theorem quotient_group.open_coe

deleted theorem quotient_group_saturate

deleted theorem quotient_ring.is_open_map_coe

deleted theorem quotient_ring.quotient_map_coe_coe

deleted theorem quotient_ring_saturate

deleted theorem uniform_space.ring_sep_quot

deleted theorem uniform_space.ring_sep_rel

deleted def uniform_space.sep_quot_equiv_ring_quot

deleted theorem {u}

Created src/topology/algebra/ring.lean

added def ideal.closure

added theorem ideal.coe_closure

added theorem quotient_ring.is_open_map_coe

added theorem quotient_ring.quotient_map_coe_coe

added theorem quotient_ring_saturate

Created src/topology/algebra/uniform_group.lean

added theorem add_comm_group.is_Z_bilin.neg_left

added theorem add_comm_group.is_Z_bilin.neg_right

added theorem add_comm_group.is_Z_bilin.sub_left

added theorem add_comm_group.is_Z_bilin.sub_right

added theorem add_comm_group.is_Z_bilin.zero

added theorem add_comm_group.is_Z_bilin.zero_left

added theorem add_comm_group.is_Z_bilin.zero_right

added theorem dense_embedding.continuous_extend_of_cauchy

added theorem dense_embedding.extend_Z_bilin

added theorem group_separation_rel

added theorem is_Z_bilin.tendsto_zero_left

added theorem is_Z_bilin.tendsto_zero_right

added theorem tendsto_sub_comap_self

added theorem to_uniform_space_eq

added def topological_add_group.to_uniform_space

added theorem topological_add_group_is_uniform

added theorem uniform_add_group.mk'

added theorem uniform_continuous_add'

added theorem uniform_continuous_add

added theorem uniform_continuous_neg'

added theorem uniform_continuous_neg

added theorem uniform_continuous_of_continuous

added theorem uniform_continuous_of_tendsto_zero

added theorem uniform_continuous_sub'

added theorem uniform_continuous_sub

added theorem uniform_embedding_translate

added theorem uniformity_eq_comap_nhds_zero'

added theorem uniformity_eq_comap_nhds_zero

added theorem uniformity_translate

Created src/topology/algebra/uniform_ring.lean

added theorem uniform_space.completion.coe_mul

added theorem uniform_space.completion.coe_one

added theorem uniform_space.completion.continuous_mul'

added theorem uniform_space.completion.continuous_mul

added theorem uniform_space.ring_sep_quot

added theorem uniform_space.ring_sep_rel

added def uniform_space.sep_quot_equiv_ring_quot

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/instances/polynomial.lean

Modified src/topology/instances/real.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/metric_space/emetric_space.lean

Modified src/topology/uniform_space/basic.lean

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_map_iff_exists_tendsto

deleted theorem cauchy_nhds

deleted theorem cauchy_of_totally_bounded_of_ultrafilter

deleted theorem cauchy_prod

deleted theorem cauchy_pure

deleted def cauchy_seq

deleted theorem cauchy_seq_iff_prod_map

deleted theorem cauchy_seq_tendsto_of_complete

deleted theorem closure_image_mem_nhds_of_uniform_embedding

deleted theorem compact_iff_totally_bounded_complete

deleted theorem compact_of_totally_bounded_is_closed

deleted theorem complete_space_extension

deleted theorem complete_space_of_is_complete_univ

deleted theorem complete_univ

deleted theorem dense_embedding.continuous_extend_of_cauchy

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_iff_adhp_of_cauchy

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_iff_filter

deleted theorem totally_bounded_iff_subset

deleted theorem totally_bounded_iff_ultrafilter

deleted theorem totally_bounded_image

deleted theorem totally_bounded_preimage

deleted theorem totally_bounded_subset

deleted theorem uniform_continuous_uniformly_extend

deleted theorem uniform_embedding.dense_embedding

deleted theorem uniform_embedding.embedding

deleted theorem uniform_embedding.prod

deleted theorem uniform_embedding.uniform_continuous

deleted theorem uniform_embedding.uniform_continuous_iff

deleted def uniform_embedding

deleted theorem uniform_embedding_comap

deleted theorem uniform_embedding_def'

deleted theorem uniform_embedding_def

deleted theorem uniform_embedding_subtype_emb

deleted theorem uniform_extend_subtype

deleted theorem uniformly_extend_exists

deleted theorem uniformly_extend_of_emb

deleted theorem uniformly_extend_spec

Created src/topology/uniform_space/cauchy.lean

added def cauchy

added theorem cauchy_comap

added theorem cauchy_downwards

added theorem cauchy_iff

added theorem cauchy_iff_exists_le_nhds

added theorem cauchy_map

added theorem cauchy_map_iff

added theorem cauchy_map_iff_exists_tendsto

added theorem cauchy_nhds

added theorem cauchy_of_totally_bounded_of_ultrafilter

added theorem cauchy_prod

added theorem cauchy_pure

added def cauchy_seq

added theorem cauchy_seq_iff_prod_map

added theorem cauchy_seq_tendsto_of_complete

added theorem compact_iff_totally_bounded_complete

added theorem compact_of_totally_bounded_is_closed

added theorem complete_space_of_is_complete_univ

added theorem complete_univ

added def is_complete

added theorem is_complete_of_is_closed

added theorem le_nhds_iff_adhp_of_cauchy

added theorem le_nhds_lim_of_cauchy

added theorem le_nhds_of_cauchy_adhp

added def totally_bounded

added theorem totally_bounded_closure

added theorem totally_bounded_empty

added theorem totally_bounded_iff_filter

added theorem totally_bounded_iff_subset

added theorem totally_bounded_iff_ultrafilter

added theorem totally_bounded_image

added theorem totally_bounded_subset

Created src/topology/uniform_space/complete_separated.lean

added theorem is_closed_of_is_complete

Modified src/topology/uniform_space/completion.lean

deleted theorem add_comm_group.is_Z_bilin.neg_left

deleted theorem add_comm_group.is_Z_bilin.neg_right

deleted theorem add_comm_group.is_Z_bilin.sub_left

deleted theorem add_comm_group.is_Z_bilin.sub_right

deleted theorem add_comm_group.is_Z_bilin.zero

deleted theorem add_comm_group.is_Z_bilin.zero_left

deleted theorem add_comm_group.is_Z_bilin.zero_right

deleted theorem dense_embedding.extend_Z_bilin

deleted theorem is_Z_bilin.tendsto_zero_left

deleted theorem is_Z_bilin.tendsto_zero_right

deleted theorem tendsto_sub_comap_self

deleted theorem uniform_space.comap_quotient_eq_uniformity

deleted theorem uniform_space.comap_quotient_le_uniformity

deleted theorem uniform_space.completion.coe_add

deleted theorem uniform_space.completion.coe_mul

deleted theorem uniform_space.completion.coe_neg

deleted theorem uniform_space.completion.coe_one

deleted theorem uniform_space.completion.coe_zero

deleted theorem uniform_space.completion.continuous_mul'

deleted theorem uniform_space.completion.continuous_mul

deleted theorem uniform_space.completion.is_add_group_hom_extension

deleted theorem uniform_space.completion.is_add_group_hom_map

deleted theorem uniform_space.completion.is_add_group_hom_prod

deleted theorem uniform_space.eq_of_separated_of_uniform_continuous

deleted theorem uniform_space.separated_of_uniform_continuous

deleted theorem uniform_space.separation_prod

deleted def uniform_space.separation_quotient.lift

deleted theorem uniform_space.separation_quotient.lift_mk

deleted def uniform_space.separation_quotient.map

deleted theorem uniform_space.separation_quotient.map_comp

deleted theorem uniform_space.separation_quotient.map_id

deleted theorem uniform_space.separation_quotient.map_mk

deleted theorem uniform_space.separation_quotient.map_unique

deleted theorem uniform_space.separation_quotient.uniform_continuous_lift

deleted theorem uniform_space.separation_quotient.uniform_continuous_map

deleted def uniform_space.separation_quotient

deleted def uniform_space.separation_setoid

deleted theorem uniform_space.uniform_continuous_quotient

deleted theorem uniform_space.uniform_continuous_quotient_lift

deleted theorem uniform_space.uniform_continuous_quotient_lift₂

deleted theorem uniform_space.uniform_continuous_quotient_mk

deleted theorem uniform_space.uniformity_quotient

Created src/topology/uniform_space/separation.lean

added def separated

added theorem separated_def'

added theorem separated_def

added theorem separated_equiv

added theorem uniform_space.comap_quotient_eq_uniformity

added theorem uniform_space.comap_quotient_le_uniformity

added theorem uniform_space.eq_of_separated_of_uniform_continuous

added theorem uniform_space.separated_of_uniform_continuous

added theorem uniform_space.separation_prod

added def uniform_space.separation_quotient.lift

added theorem uniform_space.separation_quotient.lift_mk

added def uniform_space.separation_quotient.map

added theorem uniform_space.separation_quotient.map_comp

added theorem uniform_space.separation_quotient.map_id

added theorem uniform_space.separation_quotient.map_mk

added theorem uniform_space.separation_quotient.map_unique

added theorem uniform_space.separation_quotient.uniform_continuous_lift

added theorem uniform_space.separation_quotient.uniform_continuous_map

added def uniform_space.separation_quotient

added def uniform_space.separation_setoid

added theorem uniform_space.uniform_continuous_quotient

added theorem uniform_space.uniform_continuous_quotient_lift

added theorem uniform_space.uniform_continuous_quotient_lift₂

added theorem uniform_space.uniform_continuous_quotient_mk

added theorem uniform_space.uniformity_quotient

Created src/topology/uniform_space/uniform_embedding.lean

added theorem closure_image_mem_nhds_of_uniform_embedding

added theorem complete_space_extension

added theorem is_complete_image_iff

added theorem totally_bounded_preimage

added theorem uniform_continuous_uniformly_extend

added theorem uniform_embedding.dense_embedding

added theorem uniform_embedding.embedding

added theorem uniform_embedding.prod

added theorem uniform_embedding.uniform_continuous

added theorem uniform_embedding.uniform_continuous_iff

added def uniform_embedding

added theorem uniform_embedding_comap

added theorem uniform_embedding_def'

added theorem uniform_embedding_def

added theorem uniform_embedding_subtype_emb

added theorem uniform_extend_subtype

added theorem uniformly_extend_exists

added theorem uniformly_extend_of_emb

added theorem uniformly_extend_spec