-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(SimpleGraph): independent sets #18218
base: master
Are you sure you want to change the base?
Conversation
PR summary e2f3d3f070
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Combinatorics.SimpleGraph.Clique | 553 | 561 | +8 (+1.45%) |
Import changes for all files
Files | Import difference |
---|---|
Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Turan |
6 |
Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite |
7 |
Mathlib.Combinatorics.SimpleGraph.Clique |
8 |
Mathlib.Combinatorics.SimpleGraph.IndependentSet |
562 |
Declarations diff
+ IndependentSetFree
+ IndependentSetFree.cliqueFreeOn
+ IndependentSetFree.comap
+ IndependentSetFree.mono
+ IndependentSetFree.mono'
+ IndependentSetFree.sup_edge
+ IndependentSetFreeOn
+ IndependentSetFreeOn.anti
+ IndependentSetFreeOn.mono
+ IndependentSetFreeOn.of_succ
+ IndependentSetFreeOn.subset
+ IsIndependentSet
+ IsIndependentSet.anti
+ IsIndependentSet.finsetMap
+ IsIndependentSet.insert
+ IsIndependentSet.map
+ IsIndependentSet.of_subsingleton
+ IsIndependentSet.subset
+ IsIndependentSet.subsingleton
+ IsNIndependentSet
+ IsNIndependentSet.anti
+ IsNIndependentSet.insert
+ IsNIndependentSet.map
+ IsNIndependentSet.not_independentSetFree
+ _
+ botEmbeddingOfNotIndependentSetFree
+ card_independentSetFinset_le
+ cliqueFreeOn_empty
+ cliqueFreeOn_of_card_lt
+ cliqueFreeOn_singleton
+ cliqueFreeOn_two
+ cliqueFreeOn_univ
+ cliqueNum
+ clique_card_le_cliqueNum
+ cocliqueNum
+ cocliqueNum_eq_compl_cliqueNum
+ coe_independentSetFinset
+ fintype_cliqueNum_bddAbove
+ fintype_cocliqueNum_bddAbove
+ independentSetFinset
+ independentSetFinset_anti
+ independentSetFinset_eq_empty_iff
+ independentSetFinset_map
+ independentSetFinset_map_of_equiv
+ independentSetFree_iff
+ independentSetFree_map_if
+ independentSetFree_of_card_lt
+ independentSetFree_top
+ independentSetFree_two
+ independentSetSet
+ independentSetSet_anti
+ independentSetSet_anti'
+ independentSetSet_eq_empty_iff
+ independentSetSet_map
+ independentSetSet_map_of_equiv
+ independentSetSet_one
+ independentSetSet_top
+ independentSetSet_zero
+ independentSet_card_le_cocliqueNum
+ induce_compl_eq_compl_induce
+ instance [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} {s : Finset α} :
+ instance [DecidableEq α] [DecidableRel G.Adj] {s : Finset α} : Decidable (G.IsIndependentSet s)
+ is3IndependentSet_iff
+ is3IndependentSet_triple_iff
+ isClique_compl_map_iff_isClique_map_compl
+ isIndependentSetFree_iff_isCliqueFree_of_complement
+ isIndependentSet_empty
+ isIndependentSet_iff
+ isIndependentSet_iff_induce_eq
+ isIndependentSet_iff_isClique_of_complement
+ isIndependentSet_insert
+ isIndependentSet_map_image_iff
+ isIndependentSet_pair
+ isIndependentSet_singleton
+ isIndependentSet_top_iff
+ isMaximalClique
+ isMaximalIndependentSet
+ isMaximalIndependentSet_iff_compl_isMaximalClique
+ isMaximumClique
+ isMaximumIndependentSet
+ isMaximumIndependentSet_iff_compl_isMaximumClique
+ isNIndependentSet_empty
+ isNIndependentSet_iff
+ isNIndependentSet_iff_isNClique_of_complement
+ isNIndependentSet_one
+ isNIndependentSet_singleton
+ isNIndependentSet_top_iff
+ isNIndependentSet_zero
+ map_compl_le_compl_map
+ maximalClique_if_maximumClique
+ maximalIndependentSet_if_maximumIndependentSet
+ maximumClique_card_eq_cliqueNum
+ maximumIndependentSet_card_eq_cocliqueNum
+ mem_independentSetFinset_iff
+ mem_independentSetSet_iff
+ not_independentSetFree_card_of_bot_embedding
+ not_independentSetFree_iff
+ not_independentSetFree_of_bot_embedding
++ ⟨_,
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh
contains some details about this script.
bot fix style |
repeat rw [isClique_iff, Set.Pairwise] | ||
rw [forall₂_congr]; intro a ha | ||
rw [forall₂_congr]; intro b hb | ||
rw [←imp_congr_right]; intro hab |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] reported by reviewdog 🐶
rw [←imp_congr_right]; intro hab | |
rw [← imp_congr_right]; intro hab |
feat: SimpleGraph independent sets