Commit 2026-05-31 19:36 e84ffd3b

View on Github →

feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques (#35619) Plus a couple of lemmas.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.IsClique.inter_left

added theorem SimpleGraph.IsClique.inter_right

added theorem SimpleGraph.induce_eq_top

added theorem SimpleGraph.isClique_iUnion

modified theorem SimpleGraph.isClique_iff_induce_eq

added theorem SimpleGraph.isClique_sUnion

added theorem SimpleGraph.isClique_univ

Modified Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

Modified Mathlib/Data/Set/Pairwise/Basic.lean

added theorem Set.Pairwise.inter_left

added theorem Set.Pairwise.inter_right