Mathlib Changelog
v3
Changelog
About
Github
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