Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-22 14:51 c59dbf3d

View on Github →

chore(topology/basic): add cluster_pt.map, rename mem_closure (#5065)

  • add filter.prod_pure, filter.pure_prod, cluster_pt.map, and set.maps_to.closure;
  • rename mem_closure to map_mem_closure;
  • rename mem_closure2 to map_mem_closure2.

Estimated changes

added theorem filter.prod_pure
modified theorem filter.prod_pure_pure
added theorem filter.pure_prod
added theorem cluster_pt.map
added theorem map_mem_closure
deleted theorem mem_closure
added theorem set.maps_to.closure
added theorem map_mem_closure2
deleted theorem mem_closure2