Skip to content

Commit 0301e4e

Browse files
dupuisfChrisHughes24Ruben-VandeVeldejcommelin
committed
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>
1 parent b5ff35f commit 0301e4e

File tree

2 files changed

+1190
-0
lines changed

2 files changed

+1190
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -356,6 +356,7 @@ import Mathlib.Data.Set.Lattice
356356
import Mathlib.Data.Set.NAry
357357
import Mathlib.Data.Set.Opposite
358358
import Mathlib.Data.Set.Pairwise
359+
import Mathlib.Data.Set.Pointwise.Basic
359360
import Mathlib.Data.Set.Prod
360361
import Mathlib.Data.Set.Sigma
361362
import Mathlib.Data.Set.UnionLift

0 commit comments

Comments
 (0)