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/set/intervals/pi): lemmas about intervals in Π i, π i
#4951
Conversation
Also add missing lemmas `Ixx_mem_nhds` and lemmas `pi_Ixx_mem_nhds`. For each `pi_Ixx_mem_nhds` I add a non-dependent version `pi_Ixx_mem_nhds'` because sometimes Lean fails to unify different instances while trying to apply the dependent version to `ι → ℝ`.
Could you please put that explanation somewhere in the file? bors d+ |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
bors merge |
Pull request successfully merged into master. Build succeeded: |
Π i, π i
Π i, π i
Also add missing lemmas
Ixx_mem_nhds
and lemmaspi_Ixx_mem_nhds
.For each
pi_Ixx_mem_nhds
I add a non-dependent versionpi_Ixx_mem_nhds'
because sometimes Lean fails to unify differentinstances while trying to apply the dependent version to
ι → ℝ
.