Mathlib Changelog
Changelog
About
Github
Commit
2018-10-15 13:33
fbb6e9bc
View on Github →
feat(analysis/topology): group completion
Estimated changes
Modified
analysis/real.lean
deleted
theorem
real.Cauchy_eq
Created
analysis/topology/complete_groups.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.extend_Z_bilin
added
theorem
is_Z_bilin.tendsto_zero_left
added
theorem
is_Z_bilin.tendsto_zero_right
added
theorem
tendsto_sub_comap_self
Created
analysis/topology/completion.lean
added
theorem
Cauchy.Cauchy_eq
added
theorem
Cauchy.dense_embedding_pure_cauchy
added
def
Cauchy.extend
added
theorem
Cauchy.extend_pure_cauchy
added
def
Cauchy.gen
added
theorem
Cauchy.injective_separated_pure_cauchy
added
theorem
Cauchy.mem_uniformity'
added
theorem
Cauchy.mem_uniformity
added
theorem
Cauchy.monotone_gen
added
theorem
Cauchy.nonempty_Cauchy_iff
added
def
Cauchy.prod
added
theorem
Cauchy.prod_pure_cauchy_pure_cauchy
added
def
Cauchy.pure_cauchy
added
theorem
Cauchy.pure_cauchy_dense
added
theorem
Cauchy.uniform_continuous_extend
added
theorem
Cauchy.uniform_continuous_prod
added
theorem
Cauchy.uniform_embedding_pure_cauchy
added
def
Cauchy
added
theorem
filter.prod_pure_pure
added
theorem
uniform_space.cauchy_prod
added
theorem
uniform_space.comap_quotient_eq_uniformity
added
theorem
uniform_space.comap_quotient_le_uniformity
added
theorem
uniform_space.complete_space_separation
added
theorem
uniform_space.completion.coe_add
added
theorem
uniform_space.completion.coe_neg
added
theorem
uniform_space.completion.coe_zero
added
theorem
uniform_space.completion.comap_coe_eq_uniformity
added
theorem
uniform_space.completion.continuous_coe
added
theorem
uniform_space.completion.continuous_extension
added
theorem
uniform_space.completion.continuous_map
added
theorem
uniform_space.completion.continuous_map₂
added
theorem
uniform_space.completion.dense
added
theorem
uniform_space.completion.dense₂
added
theorem
uniform_space.completion.dense₃
added
theorem
uniform_space.completion.extension_coe
added
theorem
uniform_space.completion.induction_on
added
theorem
uniform_space.completion.induction_on₂
added
theorem
uniform_space.completion.induction_on₃
added
theorem
uniform_space.completion.induction_on₄
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
added
theorem
uniform_space.completion.map_coe
added
theorem
uniform_space.completion.map₂_coe_coe
added
theorem
uniform_space.completion.prod_coe_coe
added
theorem
uniform_space.completion.uniform_continuous_coe
added
theorem
uniform_space.completion.uniform_continuous_extension
added
theorem
uniform_space.completion.uniform_continuous_map
added
theorem
uniform_space.completion.uniform_continuous_map₂'
added
theorem
uniform_space.completion.uniform_continuous_prod
added
theorem
uniform_space.completion.uniform_embedding_coe
added
def
uniform_space.completion
added
theorem
uniform_space.eq_of_separated_of_uniform_continuous
added
theorem
uniform_space.separated_of_uniform_continuous
added
theorem
uniform_space.separated_separation
added
theorem
uniform_space.separation_prod
added
def
uniform_space.separation_setoid
added
theorem
uniform_space.uniform_continuous_of_const
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
Modified
analysis/topology/continuity.lean
modified
theorem
dense_embedding.extend_e_eq
modified
theorem
dense_embedding.extend_eq
added
theorem
embedding.closure_eq_preimage_closure_image
Created
analysis/topology/topological_groups.lean
added
theorem
half_nhd
added
theorem
nhds_translation
added
theorem
nhds_zero_symm
added
theorem
quarter_nhd
added
def
topological_add_group.to_uniform_space
added
theorem
uniformity_eq_comap_nhds_zero
added
def
Δ
added
def
δ
Modified
analysis/topology/topological_structures.lean
deleted
theorem
dense_or_discrete
added
theorem
group_separation_rel
modified
theorem
uniform_continuous_add'
modified
theorem
uniform_continuous_add
modified
theorem
uniform_continuous_neg'
modified
theorem
uniform_continuous_neg
added
theorem
uniform_continuous_of_continuous
added
theorem
uniform_continuous_of_tendsto_zero
modified
theorem
uniform_continuous_sub'
modified
theorem
uniform_continuous_sub
added
theorem
uniform_embedding_translate
added
theorem
uniformity_eq_comap_nhds_zero
added
theorem
uniformity_translate
Modified
analysis/topology/uniform_space.lean
deleted
def
Cauchy.gen
deleted
theorem
Cauchy.injective_separated_pure_cauchy
deleted
theorem
Cauchy.mem_uniformity'
deleted
theorem
Cauchy.mem_uniformity
deleted
theorem
Cauchy.monotone_gen
deleted
def
Cauchy.pure_cauchy
deleted
theorem
Cauchy.pure_cauchy_dense
deleted
theorem
Cauchy.uniform_embedding_pure_cauchy
deleted
def
Cauchy
added
theorem
cauchy_prod
deleted
theorem
comap_quotient_eq_uniformity
deleted
theorem
comap_quotient_le_uniformity
deleted
theorem
complete_space_separation
added
theorem
dense_embedding.continuous_extend_of_cauchy
deleted
theorem
eq_of_separated_of_uniform_continuous
added
theorem
mem_uniformity_of_uniform_continuous_invarant
deleted
theorem
separated_of_uniform_continuous
deleted
theorem
separated_separation
deleted
theorem
separation_prod
added
theorem
uniform_continuous_of_const
deleted
theorem
uniform_continuous_quotient
deleted
theorem
uniform_continuous_quotient_lift
deleted
theorem
uniform_continuous_quotient_lift₂
deleted
theorem
uniform_continuous_quotient_mk
modified
theorem
uniform_continuous_uniformly_extend
added
theorem
uniform_embedding.embedding
deleted
theorem
uniformity_quotient
modified
theorem
uniformly_extend_exists
modified
theorem
uniformly_extend_of_emb
modified
theorem
uniformly_extend_spec
Modified
data/set/basic.lean
added
theorem
set.prod_quotient_preimage_eq_image
Modified
data/set/lattice.lean
added
theorem
set.preimage_Inter
added
theorem
set.preimage_bInter
Modified
order/basic.lean
added
theorem
dense_or_discrete