feat: port Data.Set.Pointwise.Basic (#1188)

- [x] depends on: leanprover-community/batteries#83 - [x] depends on: leanprover-community/aesop#38 - [x] depends on: #1447 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Jan 23, 2023 · 64f784b · 64f784b
1 parent c26e8e0
commit 64f784b
Show file tree

Hide file tree

Showing 2 changed files with 1,190 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -357,6 +357,7 @@ import Mathlib.Data.Set.Lattice
 import Mathlib.Data.Set.NAry
 import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Pairwise
+import Mathlib.Data.Set.Pointwise.Basic
 import Mathlib.Data.Set.Prod
 import Mathlib.Data.Set.Sigma
 import Mathlib.Data.Set.UnionLift