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(model_theory/direct_limit): Direct limits of first-order structures #11789
Conversation
This PR/issue depends on:
|
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.
LGTM, some minor comments
|
||
lemma fintype.exists_le [nonempty α] [preorder α] [is_directed α (≤)] | ||
{β : Type*} [fintype β] (f : β → α) : | ||
∃ M, ∀ i, (f i) ≤ M := |
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.
This is usually written as bdd_above (range f)
(but it's not definitionally equal)
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 think I'll add a bdd_above (range f)
version of this, but I'll leave this one in analogy to https://leanprover-community.github.io/mathlib_docs/data/finset/order.html#finset.exists_le which is the lemma used by most of the algebra library for about this purpose.
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 will also briefly look into which version works better for my purposes later... if I'm unsure, I will push the version with bdd_above
and upper_bounds
and I can revert it if it's worse.
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 have now pushed a version in terms of bdd_above
.
bors merge |
…res (#11789) Constructs the direct limit of a directed system of first-order embeddings
Pull request successfully merged into master. Build succeeded: |
Constructs the direct limit of a directed system of first-order embeddings