Zulip Chat Archive

Stream: maths

Topic: Chain lemmas


Violeta Hernández (Dec 07 2021 at 17:49):

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 (Dec 07 2021 at 17:50):

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

Violeta Hernández (Dec 07 2021 at 17:51):

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

Bryan Gin-ge Chen (Dec 07 2021 at 17:51):

No worries, thanks for contributing!


Last updated: Dec 20 2023 at 11:08 UTC