-
Notifications
You must be signed in to change notification settings - Fork 297
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
[Merged by Bors] - feat(combinatorics/simple_graph): More clique lemmas #19203
Conversation
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.
Looks good design-wise. I'll leave it to @eric-wieser
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.
LGTM
bors merge
More lemmas about `is_clique`, `is_n_clique`, `edge_set`. Also define `clique_free_on`, a local version of `clique_free`.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits) feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087) feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203) feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976) move old README.md to OLD_README.md doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243) feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028) feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629) feat(probability/independence): Independence of singletons (leanprover-community#18506) feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612) feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989) chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628) feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926) feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352) feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797) feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925) feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863) feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236) feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828) feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260) feat(tactic/positivity): Extension for `ite` (leanprover-community#17650) ... # Conflicts: # README.md
More lemmas about
is_clique
,is_n_clique
,edge_set
. Also defineclique_free_on
, a local version ofclique_free
.clique_free_on
is to be used in John Talbot's formalisation of Turán's theorem.