[Merged by Bors] - feat: The Kruskal-Katona theorem#15000
Closed
YaelDillies wants to merge 9 commits intomasterfrom
Closed
[Merged by Bors] - feat: The Kruskal-Katona theorem#15000YaelDillies wants to merge 9 commits intomasterfrom
YaelDillies wants to merge 9 commits intomasterfrom
Conversation
PR summary c9d145fb02Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
b-mehta
reviewed
Aug 5, 2024
Prove the Kruskal-Katona and Erdős–Ko–Rado theorems. From LeanCamCombi Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
f7ce83b to
9d88093
Compare
1 task
b-mehta
reviewed
Aug 11, 2024
Contributor
|
Annoying. Let's at least make sure this issue is logged somewhere else -
even if only on zulip - and not just in this file
…On Sun, 11 Aug 2024, 23:06 Yaël Dillies, ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
<#15000 (comment)>
:
> + sdiff_nonempty.2 fun h ↦ hAB.symm $ eq_of_subset_of_card_le h hAB'.le
+ have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset
+ have smaller : max' _ hV < max' _ hU := by
+ obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
+ · rw [← compress_sdiff_sdiff A B] at hAB hBA
+ cases hBA.not_lt $ toColex_compress_lt_toColex hlt hAB
+ · exact (disjoint_right.1 disj (max'_mem _ hU) $ heq.symm ▸ max'_mem _ _).elim
+ · assumption
+ refine hB ?_
+ rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]
+ exact mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩)
+
+attribute [-instance] Fintype.decidableForallFintype
+
+-- TODO: There's currently a diamond
+-- import Mathlib.Data.Fin.Basic
It's a bit of a mix since it goes through LinearOrder.liftWithOrd which
is in mathlib, but the original sin is that instDecidableEqFin does not
agree with decidable_of_iff, and both of these are in core
—
Reply to this email directly, view it on GitHub
<#15000 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHESIOUVABVCSC3UDCFI4VLZQ7N6PAVCNFSM6AAAAABLHQ6LVOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDEMZRHA4TQNZYGM>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
b-mehta
approved these changes
Aug 11, 2024
Contributor
b-mehta
left a comment
There was a problem hiding this comment.
LGTM. Let's make sure to get another review on this though, again I wrote too much of it!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by b-mehta. |
3 tasks
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 23, 2024
Prove the Kruskal-Katona and Erdős–Ko–Rado theorems. From LeanCamCombi Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Contributor
|
Build failed: |
Contributor
|
bors r+ |
Contributor
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 24, 2024
Prove the Kruskal-Katona theorem. From LeanCamCombi Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
Prove the Kruskal-Katona theorem. From LeanCamCombi Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
Prove the Kruskal-Katona theorem. From LeanCamCombi Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 12, 2024
Prove the Kruskal-Katona theorem. From LeanCamCombi Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Prove the Kruskal-Katona theorem.
From LeanCamCombi
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com