[Merged by Bors] - feat(Topology/Order/NhdsSet): new file

[urkud]

Prove lemmas about neighborhoods of intervals.

Some lemmas are TC-generalizations
of lemmas from the Sphere Eversion Project.

---

I'm adding more lemmas

[ADedecker]

This would be an iff in the order topology, right? I don't want you to add it, but that makes me think that the naming of these could get quickly inconsistent. I can think of two options:

• add _iff to the iff lemmas, and add aliases for the backwards directions with the current names
• add of_lt to the ones which aren't iff, and add aliases for backwards directions of iffs with of_lt

[urkud]

I added _iff to the iff lemmas. The Ici_mem_nhdsSet_Ici is not an iff in the order topology, e.g., for a = b = 0 in Nat.

[ADedecker]

Oh right we would probably need NoBotOrder for it to work.

[ADedecker]

Oh actually you proved it at the end of the file, perfect. EDIT: and indeed, the condition that I mentioned is not enough, you have the right one.

[ADedecker]

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style