Commit 2023-01-25 17:18 26d0adfc

View on Github →

feat: port Order.Filter.Interval (#1820)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Interval.lean

added theorem Filter.HasBasis.tendstoIxxClass

added theorem Filter.tendstoIxxClass_inf

added theorem Filter.tendstoIxxClass_of_subset

added theorem Filter.tendstoIxxClass_principal