-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
functions and cardinality #556
Conversation
logic/function.lean
Outdated
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro | |||
|
|||
Miscellaneous function constructions and lemmas. | |||
-/ | |||
import logic.basic data.option.defs | |||
import logic.basic data.option.defs data.set.function |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm against importing data
(besides any defs
) in logic
It's not officially documented, but my mental model is that logic
should be mostly independent. (And then logic
-> order
-> algebra
, and only small things are imported from data
)
We could move some stuff in data.set...
to data.set.defs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it OK if I do the import in the the other direction, i.e., prove stuff on inv_fun_on in data.set.function?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I did it the other way around, proving stuff in data.set.function
Minor missing facts from the library