Mathlib v3 is deprecated. Go to Mathlib v4

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