Commit 2023-05-25 11:48 74f0a040

View on Github →

feat: forward-port PR 19070 (#4327) Forward-port leanprover-community/mathlib#19070:

  • add Filter.set_eventuallyLE_iff_mem_inf_principal, Filter.set_eventuallyLE_iff_inf_principal_le, and Filter.set_eventuallyEq_iff_inf_principal;
  • golf nhdsWithin_eq_iff_eventuallyEq and nhdsWithin_le_iff. The original PR golfs one more lemma which was already golfed to 1 line in Mathlib 4.

Estimated changes

modified theorem nhdsWithin_le_iff