Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 13:31 1e44add0

View on Github →

feat(order/filter/countable_Inter): review (#11673)

  • drop _sets in more names;
  • add filter.of_countable_Inter and instances for filter.map/filter.comap;
  • add docs.

Estimated changes

added theorem countable_Inter_mem
deleted theorem countable_Inter_mem_sets
added theorem countable_sInter_mem
deleted theorem countable_sInter_mem_sets