first attempt for proving Sperner's Theorem#7

Open

JayPiZimmermann wants to merge 26 commits intomasterfrom

Commits on Dec 10, 2024

first attempt for proving sperner theorem
Jakob Zimmermann
committed

Commits on Dec 16, 2024

Added the sketch for a second implementation of Sperner's Theorem using more mathlib functionality.
Jakob Zimmermann
committed
Made new directory for Combinatorial results
Jakob Zimmermann
committed
small correction in assumptions for chain_extension
Jakob Zimmermann
committed

Commits on Dec 17, 2024

Finished proof of chain_extension lemma
Jakob Zimmermann
committed
fix of application of the chain_extension lemma
Jakob Zimmermann
committed

Commits on Jan 8, 2025

Added short proofs for simple theorems regarding chains and changed statement of count_maxChainsThrough
Jakob Zimmermann
committed

Commits on Jan 17, 2025

initialized induction for count_maxChainsThrough
Jakob Zimmermann
committed
Added proposal definitions for chains in Finset namespace and rewritten proof using these definitions instead of the usual chain definition, that is made for general sets
Jakob Zimmermann
committed
worked on count_maxChainsThrough
Jakob Zimmermann
committed

Commits on Jan 18, 2025

cleaning up, outsourcing proof components and continuing work on count_maxChainsThrough
Jakob Zimmermann
committed
instead of .get and .get? use getElem with the get_elem_tactic
Jakob Zimmermann
committed
changed product notation in count_maxChainsThrough
Jakob Zimmermann
committed
continued work on count_maxChainsThrough
Jakob Zimmermann
committed

Commits on Jan 19, 2025

added IsChain.card_strict_mono and beginning typeclass definitions
Jakob Zimmermann
committed

Commits on Jan 23, 2025

defining small decidable instances
Jakob Zimmermann
committed
working on incident_indices_monotone_cards
Jakob Zimmermann
committed
using sorted list in induction
Jakob Zimmermann
committed
further progression with count_maxChainsThrough
Jakob Zimmermann
committed

Commits on Jan 24, 2025

working on coercion instances
Jakob Zimmermann
committed
split the code into several files. Add two files to the ToMatlib folder
Jakob Zimmermann
committed

Commits on Jan 28, 2025

continuing restructuring and adding small lemmata for mathlib
Jakob Zimmermann
committed
adding sections in Chain.lean
Jakob Zimmermann
committed

Commits on Jan 29, 2025

changed project structure and variable assumptions. Work directly on sets instead of Finsets
Jakob Zimmermann
committed

Commits on Feb 7, 2025

Added doc strings.
Jakob Zimmermann
committed
Completed doc strings.
Jakob Zimmermann
committed