Skip to content

Commit 7a4790b

Browse files
committed
feat: port Data.Set.Pointwise.Interval (#1481)
- feat: port Mathlib.Data.Set.Pointwise.Interval - Initial file copy from mathport - Mathbin -> Mathlib; add import to Mathlib.lean
1 parent 3a0c3c1 commit 7a4790b

File tree

2 files changed

+798
-0
lines changed

2 files changed

+798
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -546,6 +546,7 @@ import Mathlib.Data.Set.Pairwise
546546
import Mathlib.Data.Set.Pointwise.Basic
547547
import Mathlib.Data.Set.Pointwise.BigOperators
548548
import Mathlib.Data.Set.Pointwise.Finite
549+
import Mathlib.Data.Set.Pointwise.Interval
549550
import Mathlib.Data.Set.Pointwise.Iterate
550551
import Mathlib.Data.Set.Pointwise.ListOfFn
551552
import Mathlib.Data.Set.Pointwise.SMul

0 commit comments

Comments
 (0)