arend-lib icon indicating copy to clipboard operation
arend-lib copied to clipboard

Published 20 hours ago • verified publisher icon JetBrains

Generalize the definition of Subset

Open tonyxty opened this issue 4 years ago • 0 comments

Subsets are currently only defined for Monoids: https://github.com/JetBrains/arend-lib/blob/6be71a0b2477906448d873f07277ec3289b31796/src/Algebra/Ring/Localization.ard#L23-L32 while they can be defined for BaseSets. It goes without saying that this is useful in general.

tonyxty avatar Oct 14 '20 14:10 tonyxty