Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Extend mathlib filters to filters on posets and use this to construct completions of theories #13

Open
flypitch opened this issue Nov 6, 2018 · 0 comments
Open

Extend mathlib filters to filters on posets and use this to construct completions of theories #13

flypitch opened this issue Nov 6, 2018 · 0 comments
Assignees
@flypitch

Comments

@flypitch
Copy link
Owner

flypitch commented Nov 6, 2018 •
edited

This would be nice to have. As Floris mentioned, we can do this by identifying elements in a poset with their up-sets, and then using the existing filter machinery which is defined on set set α.
@flypitch flypitch self-assigned this Nov 6, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@flypitch flypitch

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@flypitch