Skip to content

Commit 38c5211

Browse files
j-loreauxChrisHughes24jcommelin
committed
feat: port Order.Filter.Pointwise (#1839)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
1 parent e6cffe7 commit 38c5211

File tree

2 files changed

+1399
-0
lines changed

2 files changed

+1399
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -746,6 +746,7 @@ import Mathlib.Order.Filter.Lift
746746
import Mathlib.Order.Filter.ModEq
747747
import Mathlib.Order.Filter.NAry
748748
import Mathlib.Order.Filter.Pi
749+
import Mathlib.Order.Filter.Pointwise
749750
import Mathlib.Order.Filter.Prod
750751
import Mathlib.Order.Filter.SmallSets
751752
import Mathlib.Order.Filter.Ultrafilter

0 commit comments

Comments
 (0)