first attempt for proving Sperner's Theorem

[JayPiZimmermann]

This is a first attempt in proving Sperner's Theorem using hand-crafted definitions regarding the chain-permutation-equivalences

[mo271]

Did you intend to open this as a pull request at https://github.com/mo271/FormalBook, @JayPiZimmermann ?

[FordUniver]

Did you intend to open this as a pull request at https://github.com/mo271/FormalBook, @JayPiZimmermann ?

Don't think so @mo271, we're still working on it here.

[mo271]

ok, great, I was just wondering, because it had the old copyright header, which is now also removed at my repo...

[FordUniver]

I think @JayPiZimmermann probably tried to find this repo and found yours? Any way, we'll clean up once we have sorted out the code and then we can also PR it into your repo. Though currently we're still trying to sort out how distinct the proof will end up being from the mathlib version, which should also be Lubell's proof.

[FordUniver]

@JayPiZimmermann Kannst du die PR noch mal nach folgenden Punkten überarbeiten:

1. Aktuell sind neue Dateien / Änderungen an Dateien mit drin, die nicht dazugehören. Du hast eine elan-init.sh hinzugefügt und etwas an der independent set mathlib PR Datei geändert.
2. Alle Inhalte sollten entweder self-contained in Sperner.lean sein oder ausgegliedert in kleinere Dateien in toMathlib, aus denen mathlib PRs werden sollen. Dinge nachSperner_handcrafted_definitions.lean auslagern lässt zwar Sperner.lean schöner aussehen, aber bringt am Ende nichts. Sinn ist es zu zeigen, wie aus einem sauber aufgeschriebenen Beweis ein LEAN Beweis wird: Inhalte sollten dabei entweder in mathlib PRs landen oder in einem überschaubaren und klar strukturiertem self-contained Beweis. Wir wollen keine eigene Infrastruktur aufbauen und Sachen "verstecken".
3. Kannst du bitte deinen Beweis mit den Aigner / Ziegler Beweisschritten kommentieren? Man sollte klar zuordnen können, welcher (Teil)satz für welchen Teil des Codes verantwortlich ist. Wenn das nicht geht dann sollte in 90% der Fälle der LEAN Beweis überarbeitet werden um den Textbeweis besser widerzuspiegeln.