-
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
[Merged by Bors] - feat(order/filter/interval): define class filter.is_interval_generated
#3663
Conversation
A filter `f` on a `preorder` is interval generated if each set `s ∈ f` includes an `ord_connected` | ||
subset `t ∈ f`. | ||
-/ | ||
class is_interval_generated (f : filter α) : Prop := |
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.
Would it be more consistent and efficient to also make ord_connected
a class?
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.
It has conversions to/from convex
and is_preconnected
. Another difficulty is that some lemmas (e.g., ord_connected_sUnion
) have non-instance arguments. Possibly I can make it a @[class] def
but I'd prefer not to do it right now.
filter.is_interval_generated
deps: 3618filter.is_interval_generated
bors merge |
Pull request successfully merged into master. Build succeeded: |
filter.is_interval_generated
filter.is_interval_generated
Another chunk of #3640,
depends on #3618