Commit 2023-04-14 12:58 336482e7

View on Github →

feat: port Order.Filter.ZeroAndBoundedAtFilter (#3435)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

added theorem Filter.BoundedAtFilter.neg

added theorem Filter.BoundedAtFilter.smul

added def Filter.BoundedAtFilter

added theorem Filter.ZeroAtFilter.boundedAtFilter

added theorem Filter.ZeroAtFilter.smul

added def Filter.ZeroAtFilter

added def Filter.boundedFilterSubalgebra

added def Filter.boundedFilterSubmodule

added theorem Filter.const_boundedAtFilter

added def Filter.zeroAtFilterAddSubmonoid

added def Filter.zeroAtFilterSubmodule

added theorem Filter.zero_zeroAtFilter