Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-10 23:06 df5adc5c

View on Github →

chore(topology/*): golf some proofs (#4528)

move exists_nhds_split to topology/algebra/monoid, rename to exists_nhds_one_split;
add a version exists_open_nhds_one_split;
move exists_nhds_split4 to topology/algebra/monoid, rename to exists_nhds_one_split4;
move one_open_separated_mul to topology/algebra/monoid, rename to exists_open_nhds_one_mul_subset;
add mem_prod_nhds_iff;
golf some proofs.

Estimated changes

Modified src/topology/algebra/group.lean

deleted theorem exists_nhds_split4

deleted theorem exists_nhds_split

deleted theorem one_open_separated_mul

Modified src/topology/algebra/monoid.lean

added theorem exists_nhds_one_split4

added theorem exists_nhds_one_split

added theorem exists_open_nhds_one_mul_subset

added theorem exists_open_nhds_one_split

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/constructions.lean

modified theorem exists_nhds_square

added theorem filter.has_basis.prod_nhds

added theorem mem_nhds_prod_iff