Commit 2023-12-04 18:10 2c200e2b

View on Github →

feat(Order/Filter): add Filter.tendsto_image_smallSets (#8811)

  • Add Filter.tendsto_image_smallSets and Filter.Tendsto.image_smallSets.
  • Generalize Filter.eventually_all from Type* to Sort*.
  • Protect Filter.HasBasis.smallSets.
  • Fix a porting note about Filter.eventually_smallSets: the Lean 3 proof works in Lean 4 now.

Estimated changes

modified theorem Filter.eventually_all
deleted theorem Filter.HasBasis.smallSets