[Merged by Bors] - feat(data/set/intervals/basic): collection of lemmas of the form I??_of_I??

[benjamindavidson]

Some propositions about intervals that I thought may be useful (despite their simplicity).

[urkud]

What's the added value compared to the RHS?

[benjamindavidson]

Admittedly, while these lemmas are not definitively "better" than the lemmas used to prove them, and I would understand if they were deemed not worth being added to mathlib, I feel that their usefulness comes from the fact that their RHS are not necessarily obvious choices for their proofs; in fact, library_search does not generate them. These lemmas do show up in a library_search and also provide some consistency - I think of them as to intervals what le_of_lt is to inequalities.

[bryangingechen]

@benjamindavidson The "ready-to-merge" label means that the PR has been put on the queue to be merged; usually it's added automatically by some GitHub actions scripts. The "awaiting-review" label will put the PR on the maintainers' radar.

[bryangingechen]

Actually, in this case, I see from the discussion that this should be ready to go, so I'll approve it. Thanks for the contribution!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests