Chain lemmas

Stream: maths

[Violeta Hernández]

While working on #maths > abstract polytopes, I noticed some useful results missing from zorn.lean:

• chain.empty: The empty set is always a chain.
• chain.subsingleton: A subsingleton is always a chain.
• chain.max_chain_of_chain: Any chain is contained in a maximal chain.

The first two are immediate from what has already been proven, but useful nonetheless. The last one is a consequence of Zorn's lemma and generalizes Hausdorff's maximality principle.

I'd like non-master write access on a separate branch to add these lemmas/theorems to the file. My Github username is vihdzp.

[Bryan Gin-ge Chen]

I just checked and GitHub says you already have access; I guess someone beat me to the punch!

[Violeta Hernández]

Oh! I'm really sorry, I thought I had to ask again for every separate PR.

[Bryan Gin-ge Chen]

No worries, thanks for contributing!