Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:33 7697a84d

View on Github →

feat(analysis/topology/topological_groups): construct topologies out of a group and a neighbourhood filter at 0

Estimated changes

Deleted analysis/topology/complete_groups.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

Modified analysis/topology/completion.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

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

modified theorem uniform_space.completion.dense

added theorem uniform_space.completion.dense_embedding_coe

Modified analysis/topology/topological_groups.lean

added theorem add_group_with_zero_nhd.add_Z

added theorem add_group_with_zero_nhd.exists_Z_half

added theorem add_group_with_zero_nhd.neg_Z

added theorem add_group_with_zero_nhd.nhds_eq

added theorem add_group_with_zero_nhd.nhds_zero_eq_Z

deleted theorem half_nhd

deleted theorem nhds_translation

deleted theorem nhds_zero_symm

deleted theorem quarter_nhd

added theorem to_uniform_space_eq

added theorem topological_add_group_is_uniform

added theorem uniformity_eq_comap_nhds_zero'

deleted theorem uniformity_eq_comap_nhds_zero

deleted def Δ

deleted def δ

Modified analysis/topology/topological_space.lean

Modified analysis/topology/topological_structures.lean

added theorem exists_nhds_half

added theorem exists_nhds_quarter

added theorem nhds_translation

added theorem nhds_zero_symm

Modified order/filter.lean

modified theorem filter.comap_eq_of_inverse

added theorem filter.map_eq_of_inverse