-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/nat/basic): Add two lemmas two nat/basic which are necessary for the count PR #10001
Conversation
src/data/nat/basic.lean
Outdated
lemma nat.subtype.semilattice_sup_bot_bot_apply {s : set ℕ} [decidable_pred (∈ s)] | ||
[h : nonempty s] : ((⊥ : s) : ℕ) = nat.find (nonempty_subtype.1 h) := rfl |
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.
Perhaps reverse the sides and make it a @[simp]
lemma?
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.
Well, nat.Inf is defined in terms of nat.find - do we really want to simplify nat.find into a bottom element? I assumed nat.find is a more basic concept.
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 agree with @SymmetryUnbroken, I think the lemma is better this way around.
bors d+ |
✌️ SymmetryUnbroken can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…y for the count PR (#10001) Add two lemmas proved by refl to data/nat/basic. They are needed for the count PR, and are changing a file low enogh in the import hierarchy to be a separate PR.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Canceled. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors r+ |
…y for the count PR (#10001) Add two lemmas proved by refl to data/nat/basic. They are needed for the count PR, and are changing a file low enogh in the import hierarchy to be a separate PR. Co-authored-by: SymmetryUnbroken <64909175+SymmetryUnbroken@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…y for the count PR (#10001) Add two lemmas proved by refl to data/nat/basic. They are needed for the count PR, and are changing a file low enogh in the import hierarchy to be a separate PR. Co-authored-by: SymmetryUnbroken <64909175+SymmetryUnbroken@users.noreply.github.com>
Add two lemmas proved by refl to data/nat/basic. They are needed for the count PR, and are changing a file low enogh in the import hierarchy to be a separate PR.