Skip to content

Commit

Permalink
feat: port Data.Set.Sups (#2991)
Browse files Browse the repository at this point in the history
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
  • Loading branch information
3 people committed Mar 23, 2023
1 parent 7fc680c commit 1d50362
Show file tree
Hide file tree
Showing 2 changed files with 424 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -932,6 +932,7 @@ import Mathlib.Data.Set.Pointwise.Support
import Mathlib.Data.Set.Prod
import Mathlib.Data.Set.Semiring
import Mathlib.Data.Set.Sigma
import Mathlib.Data.Set.Sups
import Mathlib.Data.Set.UnionLift
import Mathlib.Data.SetLike.Basic
import Mathlib.Data.SetLike.Fintype
Expand Down

0 comments on commit 1d50362

Please sign in to comment.