Clique

📁 Source: Mathlib/Combinatorics/SimpleGraph/Clique.lean

Statistics

Metric	Count
Definitions `CliqueFree`, `CliqueFreeOn`, `IndepSetFree`, `IndepSetFreeOn`, `IsClique`, `IsIndepSet`, `IsMaximumClique`, `IsMaximumIndepSet`, `IsNClique`, `IsNIndepSet`, `cliqueFinset`, `cliqueNum`, `cliqueSet`, `topEmbedding`, `indepNum`, `indepSetFinset`, `indepSetSet`, `instDecidableIsCliqueCoeFinsetOfDecidableEqOfDecidableRelAdj`, `instDecidableIsIndepSetCoeFinsetOfDecidableEqOfDecidableRelAdj`, `instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj`, `instDecidableIsNIndepSetOfDecidableEqOfDecidableRelAdj`, `topEmbeddingOfNotCliqueFree`	22
Theorems `anti`, `cliqueFinset`, `cliqueFreeOn`, `cliqueSet`, `comap`, `mem_of_sup_edge_isNClique`, `mono`, `replaceVertex`, `sup_edge`, `anti`, `mono`, `of_succ`, `subset`, `card_le_cliqueNum`, `finsetMap`, `insert`, `map`, `mono`, `of_induce`, `of_subsingleton`, `sdiff_of_sup_edge`, `subset`, `subsingleton`, `card_le_indepNum`, `nonempty_mem_compl_mem_edge`, `isClique`, `isMaximalClique`, `maximum`, `isIndepSet`, `isMaximalIndepSet`, `maximum`, `card_eq`, `erase_of_mem`, `erase_of_sup_edge_of_mem`, `exists_not_adj_of_cliqueFree_succ`, `insert`, `insert_erase`, `isClique`, `map`, `mono`, `not_cliqueFree`, `of_induce`, `card_eq`, `isIndepSet`, `card_cliqueFinset_le`, `cliqueFinset_eq_empty_iff`, `cliqueFinset_map`, `cliqueFinset_map_of_equiv`, `cliqueFinset_mono`, `cliqueFreeOn_empty`, `cliqueFreeOn_of_card_lt`, `cliqueFreeOn_singleton`, `cliqueFreeOn_two`, `cliqueFreeOn_univ`, `cliqueFree_bot`, `cliqueFree_compl`, `cliqueFree_completeMultipartiteGraph`, `cliqueFree_iff`, `cliqueFree_iff_top_free`, `cliqueFree_map_iff`, `cliqueFree_of_card_lt`, `cliqueFree_one`, `cliqueFree_two`, `cliqueNum_compl`, `cliqueSet_bot`, `cliqueSet_eq_empty_iff`, `cliqueSet_map`, `cliqueSet_map_of_equiv`, `cliqueSet_mono`, `cliqueSet_mono'`, `cliqueSet_one`, `cliqueSet_zero`, `coe_cliqueFinset`, `not_cliqueFree_of_infinite`, `not_cliqueFree_of_le_card`, `not_cliqueFree_of_le_enatCard`, `topEmbedding_apply_fst`, `topEmbedding_apply_snd`, `exists_isNClique_cliqueNum`, `exists_isNIndepSet_indepNum`, `exists_of_maximal_cliqueFree_not_adj`, `indepNum_compl`, `indepSetFree_compl`, `is3Clique_iff`, `is3Clique_iff_exists_cycle_length_three`, `is3Clique_triple_iff`, `isClique_bot_iff`, `isClique_compl`, `isClique_empty`, `isClique_iff`, `isClique_iff_induce_eq`, `isClique_iff_isChain_adj`, `isClique_insert`, `isClique_insert_of_notMem`, `isClique_map_finset_iff`, `isClique_map_finset_iff_of_nontrivial`, `isClique_map_iff`, `isClique_map_iff_of_nontrivial`, `isClique_map_image_iff`, `isClique_pair`, `isClique_range_copy_top`, `isClique_singleton`, `isClique_sup_edge_of_ne_iff`, `isClique_sup_edge_of_ne_sdiff`, `isIndepSet_compl`, `isIndepSet_iff`, `isIndepSet_iff_isAntichain_adj`, `isIndepSet_induce`, `isIndepSet_neighborSet_of_triangleFree`, `isMaximalClique_compl`, `isMaximalClique_iff`, `isMaximalIndepSet_compl`, `isMaximalIndepSet_iff`, `isMaximumClique_compl`, `isMaximumClique_iff`, `isMaximumIndepSet_compl`, `isMaximumIndepSet_iff`, `isNClique_bot_iff`, `isNClique_compl`, `isNClique_empty`, `isNClique_iff`, `isNClique_map_copy_top`, `isNClique_map_iff`, `isNClique_one`, `isNClique_singleton`, `isNClique_zero`, `isNIndepSet_compl`, `isNIndepSet_iff`, `isNIndepSet_induce`, `maximumClique_card_eq_cliqueNum`, `maximumClique_exists`, `maximumIndepSet_card_eq_indepNum`, `maximumIndepSet_exists`, `mem_cliqueFinset_iff`, `mem_cliqueSet_iff`, `mem_indepSetFinset_iff`, `mem_indepSetSet_iff`, `not_cliqueFree_card_of_top_embedding`, `not_cliqueFree_iff`, `not_cliqueFree_of_top_embedding`, `not_cliqueFree_zero`, `not_isClique_iff`	142
Total	164

SimpleGraph

Definitions

Name	Category	Theorems
`CliqueFree` 📖	MathDef	27 math math: `cliqueFinset_eq_empty_iff`, `cliqueFree_two`, `completeMultipartiteGraph.not_cliqueFree_of_le_card`, `not_cliqueFree_of_top_embedding`, `not_cliqueFree_zero`, `turanGraph_cliqueFree`, `FarFromTriangleFree.not_cliqueFree`, `cliqueFree_bot`, `cliqueFreeOn_univ`, `cliqueFree_iff`, `cliqueFree_completeMultipartiteGraph`, `cliqueFree_of_card_lt`, `completeMultipartiteGraph.not_cliqueFree_of_le_enatCard`, `not_cliqueFree_iff`, `cliqueSet_eq_empty_iff`, `Colorable.cliqueFree`, `cliqueFree_one`, `not_cliqueFree_of_isTuranMaximal`, `not_cliqueFree_card_of_top_embedding`, `triangle_removal`, `cliqueFree_of_chromaticNumber_lt`, `IsNClique.not_cliqueFree`, `indepSetFree_compl`, `cliqueFree_compl`, `cliqueFree_map_iff`, `cliqueFree_iff_top_free`, `completeMultipartiteGraph.not_cliqueFree_of_infinite`
`CliqueFreeOn` 📖	MathDef	6 math math: `cliqueFreeOn_singleton`, `cliqueFreeOn_univ`, `CliqueFree.cliqueFreeOn`, `cliqueFreeOn_of_card_lt`, `cliqueFreeOn_empty`, `cliqueFreeOn_two`
`IndepSetFree` 📖	MathDef	2 math math: `indepSetFree_compl`, `cliqueFree_compl`
`IndepSetFreeOn` 📖	MathDef	—
`IsClique` 📖	MathDef	29 math math: `isClique_map_image_iff`, `isClique_iff_induce_eq`, `IsClique.of_subsingleton`, `isMaximumClique_iff`, `isMaximalClique_iff`, `isClique_map_finset_iff`, `isMaximalIndepSet_compl`, `isClique_singleton`, `isClique_pair`, `isClique_map_finset_iff_of_nontrivial`, `isIndepSet_compl`, `IsNClique.isClique`, `isClique_insert_of_notMem`, `IsMaximumClique.isClique`, `isMaximalClique_compl`, `isClique_compl`, `isClique_iff_isChain_adj`, `isClique_map_iff_of_nontrivial`, `isClique_iff`, `IsMaximumClique.isMaximalClique`, `isClique_bot_iff`, `isClique_range_copy_top`, `isClique_insert`, `isClique_sup_edge_of_ne_iff`, `isNClique_iff`, `not_isClique_iff`, `isClique_empty`, `isClique_universalVerts`, `isClique_map_iff`
`IsIndepSet` 📖	MathDef	16 math math: `isMaximalIndepSet_compl`, `isIndepSet_iff`, `IsMaximumIndepSet.isMaximalIndepSet`, `isNIndepSet_iff`, `isIndepSet_compl`, `IsNIndepSet.isIndepSet`, `isMaximalClique_compl`, `isClique_compl`, `isIndepSet_induce`, `isIndepSet_compl_iff_isVertexCover`, `isMaximalIndepSet_iff`, `isIndepSet_iff_isAntichain_adj`, `isMaximumIndepSet_iff`, `isIndepSet_neighborSet_of_triangleFree`, `IsMaximumIndepSet.isIndepSet`, `isVertexCover_compl`
`IsMaximumClique` 📖	CompData	4 math math: `maximumClique_exists`, `isMaximumClique_iff`, `isMaximumClique_compl`, `isMaximumIndepSet_compl`
`IsMaximumIndepSet` 📖	CompData	4 math math: `maximumIndepSet_exists`, `isMaximumIndepSet_iff`, `isMaximumClique_compl`, `isMaximumIndepSet_compl`
`IsNClique` 📖	CompData	23 math math: `isNClique_singleton`, `isNClique_compl`, `is3Clique_iff_exists_cycle_length_three`, `IsFiveWheelLike.isNClique_right`, `exists_isNClique_cliqueNum`, `TripartiteFromTriangles.is3Clique_iff`, `IsFiveWheelLike.isNClique_snd_right`, `TripartiteFromTriangles.toTriangle_is3Clique`, `isNClique_empty`, `IsFiveWheelLike.isNClique_left`, `is3Clique_iff`, `isNClique_one`, `isNClique_zero`, `mem_cliqueFinset_iff`, `isNIndepSet_compl`, `isNClique_map_copy_top`, `isNClique_map_iff`, `IsFiveWheelLike.isNClique_fst_left`, `exists_of_maximal_cliqueFree_not_adj`, `isNClique_iff`, `is3Clique_triple_iff`, `isNClique_bot_iff`, `mem_cliqueSet_iff`
`IsNIndepSet` 📖	CompData	7 math math: `isNClique_compl`, `mem_indepSetFinset_iff`, `isNIndepSet_iff`, `mem_indepSetSet_iff`, `isNIndepSet_compl`, `isNIndepSet_induce`, `exists_isNIndepSet_indepNum`
`cliqueFinset` 📖	CompOp	19 math math: `cliqueFinset_eq_empty_iff`, `EdgeDisjointTriangles.card_edgeFinset_le`, `cliqueFinset_mono`, `TripartiteFromTriangles.cliqueFinset_eq_map`, `FarFromTriangleFree.cliqueFinset_nonempty'`, `coe_cliqueFinset`, `LocallyLinear.card_edgeFinset`, `cliqueFinset_map_of_equiv`, `ruzsaSzemerediNumber_spec`, `FarFromTriangleFree.cliqueFinset_nonempty`, `cliqueFinset_map`, `TripartiteFromTriangles.cliqueFinset_eq_image`, `LocallyLinear.le_ruzsaSzemerediNumber`, `mem_cliqueFinset_iff`, `TripartiteFromTriangles.card_triangles`, `FarFromTriangleFree.le_card_cliqueFinset`, `CliqueFree.cliqueFinset`, `card_cliqueFinset_le`, `triangle_counting`
`cliqueNum` 📖	CompOp	6 math math: `cliqueNum_compl`, `exists_isNClique_cliqueNum`, `maximumClique_card_eq_cliqueNum`, `cliqueNum_le_chromaticNumber`, `IsClique.card_le_cliqueNum`, `indepNum_compl`
`cliqueSet` 📖	CompOp	15 math math: `cliqueSet_bot`, `TripartiteFromTriangles.toTriangle_surjOn`, `cliqueSet_mono`, `coe_cliqueFinset`, `cliqueSet_map_of_equiv`, `cliqueSet_mono'`, `cliqueSet_map`, `CliqueFree.cliqueSet`, `TripartiteFromTriangles.cliqueSet_eq_image`, `edgeDisjointTriangles_iff_mem_sym2_subsingleton`, `EdgeDisjointTriangles.mem_sym2_subsingleton`, `cliqueSet_eq_empty_iff`, `cliqueSet_zero`, `cliqueSet_one`, `mem_cliqueSet_iff`
`indepNum` 📖	CompOp	5 math math: `cliqueNum_compl`, `maximumIndepSet_card_eq_indepNum`, `IsIndepSet.card_le_indepNum`, `exists_isNIndepSet_indepNum`, `indepNum_compl`
`indepSetFinset` 📖	CompOp	1 math math: `mem_indepSetFinset_iff`
`indepSetSet` 📖	CompOp	1 math math: `mem_indepSetSet_iff`
`instDecidableIsCliqueCoeFinsetOfDecidableEqOfDecidableRelAdj` 📖	CompOp	—
`instDecidableIsIndepSetCoeFinsetOfDecidableEqOfDecidableRelAdj` 📖	CompOp	—
`instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj` 📖	CompOp	—
`instDecidableIsNIndepSetOfDecidableEqOfDecidableRelAdj` 📖	CompOp	—
`topEmbeddingOfNotCliqueFree` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_cliqueFinset_le` 📖	mathematical	—	`Finset.card` `Finset` `cliqueFinset` `Nat.choose` `Fintype.card`	—	`Finset.card_univ` `Finset.card_powersetCard` `Finset.card_mono` `IsNClique.card_eq`
`cliqueFinset_eq_empty_iff` 📖	mathematical	—	`cliqueFinset` `Finset` `Finset.instEmptyCollection` `CliqueFree`	—	—
`cliqueFinset_map` 📖	mathematical	—	`cliqueFinset` `map` `instDecidableMapAdj` `Relation.instDecidableMapOfExistsAndEq` `Adj` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Fintype.decidableExistsFintype` `Finset.map` `Finset` `Finset.map_injective`	—	`Finset.coe_injective` `Finset.map_injective` `coe_cliqueFinset` `cliqueSet_map` `Finset.coe_map` `Set.image_congr`
`cliqueFinset_map_of_equiv` 📖	mathematical	—	`cliqueFinset` `map` `Equiv.toEmbedding` `instDecidableMapAdj` `Relation.instDecidableMapOfExistsAndEq` `Adj` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Fintype.decidableExistsFintype` `Finset.map` `Finset` `Finset.map_injective`	—	`Finset.coe_injective` `Finset.map_injective` `coe_cliqueFinset` `Finset.coe_map` `cliqueSet_map_of_equiv`
`cliqueFinset_mono` 📖	mathematical	`SimpleGraph` `instLE`	`Finset` `Finset.instHasSubset` `cliqueFinset`	—	`Finset.monotone_filter_right` `IsNClique.mono`
`cliqueFreeOn_empty` 📖	mathematical	—	`CliqueFreeOn` `Set` `Set.instEmptyCollection`	—	—
`cliqueFreeOn_of_card_lt` 📖	mathematical	`Finset.card`	`CliqueFreeOn` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`LT.lt.not_ge` `Eq.trans_le` `IsNClique.card_eq` `Finset.card_mono`
`cliqueFreeOn_singleton` 📖	mathematical	—	`CliqueFreeOn` `Set` `Set.instSingletonSet`	—	`Finset.coe_empty` `Finset.coe_singleton` `Nat.instCanonicallyOrderedAdd` `zero_add` `Finset.card_singleton` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder`
`cliqueFreeOn_two` 📖	mathematical	—	`CliqueFreeOn` `Set.Pairwise` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `Adj`	—	`Finset.coe_insert` `Finset.coe_singleton` `Set.insert_subset_iff` `Set.singleton_subset_iff` `Adj.ne` `Finset.card_pair`
`cliqueFreeOn_univ` 📖	mathematical	—	`CliqueFreeOn` `Set.univ` `CliqueFree`	—	—
`cliqueFree_bot` 📖	mathematical	—	`CliqueFree` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`le_trans` `isNClique_bot_iff`
`cliqueFree_compl` 📖	mathematical	—	`CliqueFree` `Compl.compl` `SimpleGraph` `instCompl` `IndepSetFree`	—	—
`cliqueFree_completeMultipartiteGraph` 📖	mathematical	`Fintype.card`	`CliqueFree` `completeMultipartiteGraph`	—	`cliqueFree_iff` `isEmpty_iff` `Fintype.exists_ne_map_eq_of_card_lt` `Fintype.card_fin` `top_adj` `comap_adj` `Embedding.map_adj_iff`
`cliqueFree_iff` 📖	mathematical	—	`CliqueFree` `IsEmpty` `Embedding` `completeGraph`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `not_cliqueFree_iff`
`cliqueFree_iff_top_free` 📖	mathematical	—	`CliqueFree` `Fintype.card` `Free` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`not_iff_not` `not_free` `not_cliqueFree_iff` `isContained_congr`
`cliqueFree_map_iff` 📖	mathematical	—	`CliqueFree` `map`	—	`le_or_gt` `isNClique_map_iff`
`cliqueFree_of_card_lt` 📖	mathematical	`Fintype.card`	`CliqueFree`	—	`cliqueFree_iff` `Mathlib.Tactic.Contrapose.contrapose₁` `Fintype.card_fin` `Fintype.card_le_of_embedding`
`cliqueFree_one` 📖	mathematical	—	`CliqueFree` `IsEmpty`	—	—
`cliqueFree_two` 📖	mathematical	—	`CliqueFree` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Finset.coe_insert` `Finset.coe_singleton` `Adj.ne` `Finset.card_pair` `cliqueFree_bot` `le_rfl`
`cliqueNum_compl` 📖	mathematical	—	`cliqueNum` `Compl.compl` `SimpleGraph` `instCompl` `indepNum`	—	—
`cliqueSet_bot` 📖	mathematical	—	`cliqueSet` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Set` `Finset` `Set.instEmptyCollection`	—	`CliqueFree.cliqueSet` `cliqueFree_bot`
`cliqueSet_eq_empty_iff` 📖	mathematical	—	`cliqueSet` `Set` `Finset` `Set.instEmptyCollection` `CliqueFree`	—	—
`cliqueSet_map` 📖	mathematical	—	`cliqueSet` `map` `Set.image` `Finset` `Finset.map`	—	`Set.ext` `Function.Injective.injOn` `Function.Embedding.injective` `Finset.map_eq_image` `Finset.image_preimage` `Finset.filter_true_of_mem` `Finset.exists_mem_ne` `Ne.lt_of_le'` `Finset.card_pos` `Finset.coe_preimage` `map_adj_apply` `Finset.card_map` `IsNClique.map`
`cliqueSet_map_of_equiv` 📖	mathematical	—	`cliqueSet` `map` `Equiv.toEmbedding` `Set.image` `Finset` `Finset.map`	—	`eq_or_ne` `Set.ext` `cliqueSet_one` `Equiv.exists_congr_left` `Finset.map_singleton` `Equiv.apply_symm_apply` `cliqueSet_map`
`cliqueSet_mono` 📖	mathematical	`SimpleGraph` `instLE`	`Set` `Finset` `Set.instHasSubset` `cliqueSet`	—	`IsNClique.mono`
`cliqueSet_mono'` 📖	mathematical	`SimpleGraph` `instLE`	`Pi.hasLe` `Set` `Finset` `Set.instLE` `cliqueSet`	—	`cliqueSet_mono`
`cliqueSet_one` 📖	mathematical	—	`cliqueSet` `Set.range` `Finset` `Finset.instSingleton`	—	`Set.ext`
`cliqueSet_zero` 📖	mathematical	—	`cliqueSet` `Finset` `Set` `Set.instSingletonSet` `Finset.instEmptyCollection`	—	`Set.ext`
`coe_cliqueFinset` 📖	mathematical	—	`SetLike.coe` `Finset` `Finset.instSetLike` `cliqueFinset` `cliqueSet`	—	`Set.ext` `mem_cliqueFinset_iff`
`exists_isNClique_cliqueNum` 📖	mathematical	—	`IsNClique` `cliqueNum`	—	`Nat.sSup_mem` `csSup_of_not_bddAbove` `csSup_empty`
`exists_isNIndepSet_indepNum` 📖	mathematical	—	`IsNIndepSet` `indepNum`	—	`exists_isNClique_cliqueNum`
`exists_of_maximal_cliqueFree_not_adj` 📖	mathematical	`Maximal` `SimpleGraph` `instLE` `CliqueFree` `Adj`	`Finset` `Finset.instMembership` `IsNClique` `Finset.instInsert`	—	`not_forall_not` `Maximal.not_prop_of_gt` `lt_sup_edge` `Finset.notMem_erase` `Finset.erase_right_comm` `CliqueFree.mem_of_sup_edge_isNClique` `edge_comm` `Finset.insert_erase` `Finset.mem_erase_of_ne_of_mem` `IsNClique.erase_of_sup_edge_of_mem`
`indepNum_compl` 📖	mathematical	—	`indepNum` `Compl.compl` `SimpleGraph` `instCompl` `cliqueNum`	—	—
`indepSetFree_compl` 📖	mathematical	—	`IndepSetFree` `Compl.compl` `SimpleGraph` `instCompl` `CliqueFree`	—	—
`is3Clique_iff` 📖	mathematical	—	`IsNClique` `Adj` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`Finset.card_eq_three` `IsNClique.card_eq` `is3Clique_triple_iff`
`is3Clique_iff_exists_cycle_length_three` 📖	mathematical	—	`IsNClique` `Walk.IsCycle` `Walk.length`	—	`Adj.symm` `zero_add`
`is3Clique_triple_iff` 📖	mathematical	—	`IsNClique` `Finset` `Finset.instInsert` `Finset.instSingleton` `Adj`	—	`Finset.coe_insert` `Set.pairwise_insert_of_symmetric` `symm` `Finset.coe_singleton` `Set.insert_eq_of_mem` `Finset.insert_eq_of_mem` `Finset.card_singleton` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finset.card_insert_of_notMem`
`isClique_bot_iff` 📖	mathematical	—	`IsClique` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Set.Subsingleton`	—	`Set.pairwise_bot_iff`
`isClique_compl` 📖	mathematical	—	`IsClique` `Compl.compl` `SimpleGraph` `instCompl` `IsIndepSet`	—	`isIndepSet_iff` `isClique_iff` `Set.Pairwise.eq_1`
`isClique_empty` 📖	mathematical	—	`IsClique` `Set` `Set.instEmptyCollection`	—	—
`isClique_iff` 📖	mathematical	—	`IsClique` `Set.Pairwise` `Adj`	—	—
`isClique_iff_induce_eq` 📖	mathematical	—	`IsClique` `induce` `Top.top` `SimpleGraph` `Set.Elem` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`isClique_iff` `ext` `Adj.ne`
`isClique_iff_isChain_adj` 📖	mathematical	—	`IsClique` `IsChain` `Adj`	—	`Symmetric.iff` `symm`
`isClique_insert` 📖	mathematical	—	`IsClique` `Set` `Set.instInsert` `Adj`	—	`Set.pairwise_insert_of_symmetric` `symm`
`isClique_insert_of_notMem` 📖	mathematical	`Set` `Set.instMembership`	`IsClique` `Set.instInsert` `Adj`	—	`Set.pairwise_insert_of_symmetric_of_notMem` `symm`
`isClique_map_finset_iff` 📖	mathematical	—	`IsClique` `map` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card` `Finset.map`	—	`le_or_gt` `IsClique.of_subsingleton` `Finset.card_le_one` `isClique_map_finset_iff_of_nontrivial` `Finset.one_lt_card_iff_nontrivial` `not_lt`
`isClique_map_finset_iff_of_nontrivial` 📖	mathematical	`Finset.Nontrivial`	`IsClique` `map` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.map`	—	`isClique_map_iff_of_nontrivial` `Set.Finite.exists_finset_coe` `Set.Finite.of_finite_image` `Function.Injective.injOn` `Function.Embedding.injective` `Finset.coe_map` `IsClique.map`
`isClique_map_iff` 📖	mathematical	—	`IsClique` `map` `Set.Subsingleton` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Set.subsingleton_or_nontrivial` `isClique_map_iff_of_nontrivial` `Set.Nontrivial.not_subsingleton`
`isClique_map_iff_of_nontrivial` 📖	mathematical	`Set.Nontrivial`	`IsClique` `map` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Function.instEmbeddingLikeEmbedding` `EmbeddingLike.apply_eq_iff_eq` `Set.image_preimage_eq_iff` `Set.Nontrivial.exists_ne` `Set.mem_range_self` `IsClique.map`
`isClique_map_image_iff` 📖	mathematical	—	`IsClique` `map` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`isClique_map_iff` `Function.Injective.subsingleton_image_iff` `Function.Embedding.injective` `Set.subsingleton_or_nontrivial` `Set.image_eq_image` `Set.Nontrivial.not_subsingleton`
`isClique_pair` 📖	mathematical	—	`IsClique` `Set` `Set.instInsert` `Set.instSingletonSet` `Adj`	—	`Set.pairwise_pair_of_symmetric` `symm`
`isClique_range_copy_top` 📖	mathematical	—	`IsClique` `Set.range` `DFunLike.coe` `Copy` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Copy.instFunLike`	—	`Copy.topEmbedding_apply` `Embedding.map_adj_iff` `top_adj` `Iff.ne` `Function.Embedding.apply_eq_iff_eq` `RelEmbedding.coe_toEmbedding`
`isClique_singleton` 📖	mathematical	—	`IsClique` `Set` `Set.instSingletonSet`	—	—
`isClique_sup_edge_of_ne_iff` 📖	mathematical	—	`IsClique` `SimpleGraph` `instMax` `edge` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`IsClique.sdiff_of_sup_edge` `edge_comm` `isClique_sup_edge_of_ne_sdiff`
`isClique_sup_edge_of_ne_sdiff` 📖	mathematical	`IsClique` `Set` `Set.instSDiff` `Set.instSingletonSet`	`SimpleGraph` `instMax` `edge`	—	`IsClique.mono` `le_sup_left`
`isIndepSet_compl` 📖	mathematical	—	`IsIndepSet` `Compl.compl` `SimpleGraph` `instCompl` `IsClique`	—	`isIndepSet_iff` `isClique_iff` `Set.Pairwise.eq_1`
`isIndepSet_iff` 📖	mathematical	—	`IsIndepSet` `Set.Pairwise` `Adj`	—	—
`isIndepSet_iff_isAntichain_adj` 📖	mathematical	—	`IsIndepSet` `IsAntichain` `Adj`	—	—
`isIndepSet_induce` 📖	mathematical	—	`IsIndepSet` `Set.Elem` `Subgraph.verts` `Subgraph.induce` `Top.top` `Subgraph` `Subgraph.instTop` `Subgraph.coe` `Set.image` `Set` `Set.instMembership`	—	—
`isIndepSet_neighborSet_of_triangleFree` 📖	mathematical	`CliqueFree`	`IsIndepSet` `neighborSet`	—	`Mathlib.Tactic.Push.not_forall_eq` `Set.Pairwise.eq_1` `IsIndepSet.eq_1` `is3Clique_triple_iff`
`isMaximalClique_compl` 📖	mathematical	—	`Maximal` `Set` `Set.instLE` `IsClique` `Compl.compl` `SimpleGraph` `instCompl` `SetLike.coe` `Finset` `Finset.instSetLike` `IsIndepSet`	—	—
`isMaximalClique_iff` 📖	mathematical	—	`Maximal` `Set` `Set.instLE` `IsClique` `Set.instHasSubset`	—	—
`isMaximalIndepSet_compl` 📖	mathematical	—	`Maximal` `Set` `Set.instLE` `IsIndepSet` `Compl.compl` `SimpleGraph` `instCompl` `SetLike.coe` `Finset` `Finset.instSetLike` `IsClique`	—	—
`isMaximalIndepSet_iff` 📖	mathematical	—	`Maximal` `Set` `Set.instLE` `IsIndepSet` `Set.instHasSubset`	—	—
`isMaximumClique_compl` 📖	mathematical	—	`IsMaximumClique` `Compl.compl` `SimpleGraph` `instCompl` `IsMaximumIndepSet`	—	—
`isMaximumClique_iff` 📖	mathematical	—	`IsMaximumClique` `IsClique` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	—	`IsMaximumClique.isClique` `IsMaximumClique.maximum`
`isMaximumIndepSet_compl` 📖	mathematical	—	`IsMaximumIndepSet` `Compl.compl` `SimpleGraph` `instCompl` `IsMaximumClique`	—	—
`isMaximumIndepSet_iff` 📖	mathematical	—	`IsMaximumIndepSet` `IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	—	—
`isNClique_bot_iff` 📖	mathematical	—	`IsNClique` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Finset.card`	—	`isNClique_iff` `isClique_bot_iff` `Finset.card_le_one`
`isNClique_compl` 📖	mathematical	—	`IsNClique` `Compl.compl` `SimpleGraph` `instCompl` `IsNIndepSet`	—	`isNIndepSet_iff`
`isNClique_empty` 📖	mathematical	—	`IsNClique` `Finset` `Finset.instEmptyCollection`	—	`Finset.coe_empty`
`isNClique_iff` 📖	mathematical	—	`IsNClique` `IsClique` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	—	`IsNClique.isClique` `IsNClique.card_eq`
`isNClique_map_copy_top` 📖	mathematical	—	`IsNClique` `Fintype.card` `Finset.map` `Copy.toEmbedding` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Finset.univ`	—	`isNClique_iff` `Finset.card_map` `Finset.card_univ` `Finset.coe_map` `Finset.coe_univ` `Set.image_univ` `isClique_range_copy_top`
`isNClique_map_iff` 📖	mathematical	—	`IsNClique` `map` `Finset.map`	—	`isNClique_iff` `isClique_map_finset_iff` `LE.le.not_gt` `Finset.card_map` `IsNClique.isClique` `IsNClique.card_eq`
`isNClique_one` 📖	mathematical	—	`IsNClique` `Finset` `Finset.instSingleton`	—	`Finset.coe_singleton`
`isNClique_singleton` 📖	mathematical	—	`IsNClique` `Finset` `Finset.instSingleton`	—	`Finset.coe_singleton` `Finset.card_singleton`
`isNClique_zero` 📖	mathematical	—	`IsNClique` `Finset` `Finset.instEmptyCollection`	—	`Finset.coe_empty`
`isNIndepSet_compl` 📖	mathematical	—	`IsNIndepSet` `Compl.compl` `SimpleGraph` `instCompl` `IsNClique`	—	`isNClique_iff`
`isNIndepSet_iff` 📖	mathematical	—	`IsNIndepSet` `IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	—	—
`isNIndepSet_induce` 📖	mathematical	—	`IsNIndepSet` `Set.Elem` `Subgraph.verts` `Subgraph.induce` `Top.top` `Subgraph` `Subgraph.instTop` `Subgraph.coe` `Finset.map` `Set` `Set.instMembership` `Subtype.val_injective`	—	`Subtype.val_injective` `isIndepSet_induce` `Finset.coe_map` `Set.image_congr` `Finset.card_map`
`maximumClique_card_eq_cliqueNum` 📖	mathematical	`IsMaximumClique`	`Finset.card` `cliqueNum`	—	`exists_isNClique_cliqueNum` `eq_of_le_of_not_lt` `IsClique.card_le_cliqueNum`
`maximumClique_exists` 📖	mathematical	—	`IsMaximumClique`	—	`exists_isNClique_cliqueNum` `IsNClique.isClique` `IsClique.card_le_cliqueNum` `IsNClique.card_eq`
`maximumIndepSet_card_eq_indepNum` 📖	mathematical	`IsMaximumIndepSet`	`Finset.card` `indepNum`	—	`maximumClique_card_eq_cliqueNum` `isMaximumClique_compl`
`maximumIndepSet_exists` 📖	mathematical	—	`IsMaximumIndepSet`	—	—
`mem_cliqueFinset_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `cliqueFinset` `IsNClique`	—	`Finset.mem_filter` `Finset.mem_univ`
`mem_cliqueSet_iff` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `cliqueSet` `IsNClique`	—	—
`mem_indepSetFinset_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `indepSetFinset` `IsNIndepSet`	—	`Finset.mem_filter` `Finset.mem_univ`
`mem_indepSetSet_iff` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `indepSetSet` `IsNIndepSet`	—	—
`not_cliqueFree_card_of_top_embedding` 📖	mathematical	—	`CliqueFree` `Fintype.card`	—	`not_cliqueFree_iff`
`not_cliqueFree_iff` 📖	mathematical	—	`CliqueFree` `Embedding` `completeGraph`	—	`not_cliqueFree_of_top_embedding`
`not_cliqueFree_of_top_embedding` 📖	mathematical	—	`CliqueFree`	—	`Finset.card_map` `Finset.card_fin` `ext` `Finset.coe_map` `Finset.coe_univ` `Embedding.map_adj_iff`
`not_cliqueFree_zero` 📖	mathematical	—	`CliqueFree`	—	`isNClique_empty`
`not_isClique_iff` 📖	mathematical	—	`IsClique` `Adj` `Set` `Set.instMembership`	—	—

SimpleGraph.CliqueFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.CliqueFree`	—	—	`SimpleGraph.IsNClique.mono`
`cliqueFinset` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph.cliqueFinset` `Finset` `Finset.instEmptyCollection`	—	`SimpleGraph.cliqueFinset_eq_empty_iff`
`cliqueFreeOn` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph.CliqueFreeOn`	—	—
`cliqueSet` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph.cliqueSet` `Set` `Finset` `Set.instEmptyCollection`	—	`SimpleGraph.cliqueSet_eq_empty_iff`
`comap` 📖	—	`SimpleGraph.CliqueFree`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `SimpleGraph.not_cliqueFree_of_top_embedding`
`mem_of_sup_edge_isNClique` 📖	mathematical	`SimpleGraph.CliqueFree` `SimpleGraph.IsNClique` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.edge`	`Finset` `Finset.instMembership`	—	`sdiff_eq_left` `Set.disjoint_singleton_right` `SimpleGraph.IsClique.sdiff_of_sup_edge` `SimpleGraph.IsNClique.isClique` `SimpleGraph.IsNClique.card_eq`
`mono` 📖	—	`SimpleGraph.CliqueFree`	—	—	`Finset.exists_subset_card_eq` `LE.le.trans` `Eq.ge` `SimpleGraph.IsNClique.card_eq` `SimpleGraph.IsClique.subset` `SimpleGraph.IsNClique.isClique`
`replaceVertex` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph.replaceVertex`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `SimpleGraph.not_cliqueFree_iff` `SimpleGraph.replaceVertex_self` `Function.Embedding.apply_eq_iff_eq` `SimpleGraph.adj_replaceVertex_iff_of_ne`
`sup_edge` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.edge`	—	`SimpleGraph.IsNClique.not_cliqueFree` `SimpleGraph.IsNClique.erase_of_sup_edge_of_mem` `mem_of_sup_edge_isNClique` `mono`

SimpleGraph.CliqueFreeOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.CliqueFreeOn`	—	—	`SimpleGraph.IsNClique.mono`
`mono` 📖	—	`SimpleGraph.CliqueFreeOn`	—	—	`Finset.exists_subset_card_eq` `LE.le.trans` `Eq.ge` `SimpleGraph.IsNClique.card_eq` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Finset.coe_subset` `SimpleGraph.IsClique.subset` `SimpleGraph.IsNClique.isClique`
`of_succ` 📖	mathematical	`SimpleGraph.CliqueFreeOn` `Set` `Set.instMembership`	`Set.instInter` `SimpleGraph.neighborSet`	—	`Finset.coe_insert` `Set.insert_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `SimpleGraph.IsNClique.insert`
`subset` 📖	—	`Set` `Set.instHasSubset` `SimpleGraph.CliqueFreeOn`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`

SimpleGraph.IsClique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_cliqueNum` 📖	mathematical	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card` `SimpleGraph.cliqueNum`	—	`le_csSup`
`finsetMap` 📖	mathematical	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	`SimpleGraph.map` `Finset.map`	—	`Finset.coe_map`
`insert` 📖	mathematical	`SimpleGraph.IsClique` `SimpleGraph.Adj`	`Set` `Set.instInsert`	—	`Set.Pairwise.insert_of_symmetric` `SimpleGraph.symm`
`map` 📖	mathematical	`SimpleGraph.IsClique`	`SimpleGraph.map` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	—
`mono` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsClique`	—	—	`Set.Pairwise.mono'`
`of_induce` 📖	mathematical	`SimpleGraph.IsClique` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.induce` `SimpleGraph.Subgraph.coe`	`Set.image` `Set` `Set.instMembership`	—	`SimpleGraph.Subgraph.adj_sub` `Subtype.coe_ne_coe`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton`	`SimpleGraph.IsClique`	—	`Set.Subsingleton.pairwise`
`sdiff_of_sup_edge` 📖	mathematical	`SimpleGraph.IsClique` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.edge`	`Set` `Set.instSDiff` `Set.instSingletonSet`	—	—
`subset` 📖	—	`Set` `Set.instHasSubset` `SimpleGraph.IsClique`	—	—	`Set.Pairwise.mono`
`subsingleton` 📖	mathematical	`SimpleGraph.IsClique` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra`	`Set.Subsingleton`	—	`SimpleGraph.isClique_bot_iff`

SimpleGraph.IsIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_indepNum` 📖	mathematical	`SimpleGraph.IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card` `SimpleGraph.indepNum`	—	`SimpleGraph.IsClique.card_le_cliqueNum` `SimpleGraph.isClique_compl`
`nonempty_mem_compl_mem_edge` 📖	mathematical	`SimpleGraph.IsIndepSet` `Sym2` `Set` `Set.instMembership` `SimpleGraph.edgeSet`	`Set.Nonempty` `setOf` `Compl.compl` `Set.instCompl` `SetLike.instMembership` `Sym2.instSetLike`	—	`Set.not_notMem` `Set.notMem_empty` `Sym2.mem_mk_left` `Sym2.mem_mk_right` `SimpleGraph.Adj.ne`

SimpleGraph.IsMaximumClique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClique` 📖	mathematical	`SimpleGraph.IsMaximumClique`	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`isMaximalClique` 📖	mathematical	`SimpleGraph.IsMaximumClique`	`Maximal` `Set` `Set.instLE` `SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`isClique` `Subtype.finite` `Set.coe_toFinset` `maximum` `Finset.card_lt_card` `ssubset_of_ne_of_subset` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset` `Set.subset_toFinset` `lt_irrefl` `lt_of_lt_of_le`
`maximum` 📖	mathematical	`SimpleGraph.IsMaximumClique` `SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card`	—	—

SimpleGraph.IsMaximumIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIndepSet` 📖	mathematical	`SimpleGraph.IsMaximumIndepSet`	`SimpleGraph.IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`isMaximalIndepSet` 📖	mathematical	`SimpleGraph.IsMaximumIndepSet`	`Maximal` `Set` `Set.instLE` `SimpleGraph.IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`SimpleGraph.isMaximalClique_compl` `SimpleGraph.IsMaximumClique.isMaximalClique` `SimpleGraph.isMaximumClique_compl`
`maximum` 📖	mathematical	`SimpleGraph.IsMaximumIndepSet` `SimpleGraph.IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card`	—	—

SimpleGraph.IsNClique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq` 📖	mathematical	`SimpleGraph.IsNClique`	`Finset.card`	—	—
`erase_of_mem` 📖	mathematical	`SimpleGraph.IsNClique` `Finset` `Finset.instMembership`	`Finset.erase`	—	`SimpleGraph.IsClique.subset` `Finset.coe_erase` `isClique` `Finset.card_erase_of_mem` `card_eq`
`erase_of_sup_edge_of_mem` 📖	mathematical	`SimpleGraph.IsNClique` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.edge` `Finset` `Finset.instMembership`	`Finset.erase`	—	`SimpleGraph.IsClique.sdiff_of_sup_edge` `isClique` `Finset.coe_erase` `Finset.card_erase_of_mem` `card_eq`
`exists_not_adj_of_cliqueFree_succ` 📖	mathematical	`SimpleGraph.IsNClique` `SimpleGraph.CliqueFree`	`Finset` `Finset.instMembership` `SimpleGraph.Adj`	—	`not_cliqueFree` `insert` `Mathlib.Tactic.Push.not_and_eq`
`insert` 📖	mathematical	`SimpleGraph.IsNClique` `SimpleGraph.Adj`	`Finset` `Finset.instInsert`	—	`Finset.coe_insert` `SimpleGraph.IsClique.insert` `isClique` `Finset.card_insert_of_notMem` `SimpleGraph.Adj.ne` `card_eq`
`insert_erase` 📖	mathematical	`SimpleGraph.IsNClique` `SimpleGraph.Adj` `Finset` `Finset.instMembership`	`Finset.instInsert` `Finset.erase`	—	`Finset.notMem_empty` `SimpleGraph.isNClique_zero` `insert` `erase_of_mem`
`isClique` 📖	mathematical	`SimpleGraph.IsNClique`	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`map` 📖	mathematical	`SimpleGraph.IsNClique`	`SimpleGraph.map` `Finset.map`	—	`Finset.coe_map` `SimpleGraph.IsClique.map` `isClique` `Finset.card_map` `card_eq`
`mono` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsNClique`	—	—	`SimpleGraph.IsClique.mono`
`not_cliqueFree` 📖	mathematical	`SimpleGraph.IsNClique`	`SimpleGraph.CliqueFree`	—	—
`of_induce` 📖	mathematical	`SimpleGraph.IsNClique` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.induce` `SimpleGraph.Subgraph.coe`	`Finset.map` `Set` `Set.instMembership` `Subtype.val_injective`	—	`Subtype.val_injective` `SimpleGraph.isNClique_iff` `Finset.coe_map` `Finset.card_map` `SimpleGraph.IsClique.of_induce`

SimpleGraph.IsNIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq` 📖	mathematical	`SimpleGraph.IsNIndepSet`	`Finset.card`	—	—
`isIndepSet` 📖	mathematical	`SimpleGraph.IsNIndepSet`	`SimpleGraph.IsIndepSet` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—

SimpleGraph.completeMultipartiteGraph

Definitions

Name	Category	Theorems
`topEmbedding` 📖	CompOp	2 math math: `topEmbedding_apply_fst`, `topEmbedding_apply_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_cliqueFree_of_infinite` 📖	mathematical	—	`SimpleGraph.CliqueFree` `SimpleGraph.completeMultipartiteGraph`	—	`SimpleGraph.not_cliqueFree_of_top_embedding`
`not_cliqueFree_of_le_card` 📖	mathematical	`Fintype.card`	`SimpleGraph.CliqueFree` `SimpleGraph.completeMultipartiteGraph`	—	`SimpleGraph.cliqueFree_iff` `SimpleGraph.CliqueFree.mono`
`not_cliqueFree_of_le_enatCard` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `ENat.card`	`SimpleGraph.CliqueFree` `SimpleGraph.completeMultipartiteGraph`	—	`not_cliqueFree_of_infinite` `not_cliqueFree_of_le_card` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENat.card_eq_coe_fintype_card`
`topEmbedding_apply_fst` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `SimpleGraph.Adj` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `SimpleGraph.completeMultipartiteGraph` `RelEmbedding.instFunLike` `topEmbedding`	—	—
`topEmbedding_apply_snd` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `SimpleGraph.Adj` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `SimpleGraph.completeMultipartiteGraph` `RelEmbedding.instFunLike` `topEmbedding`	—	—

---

← Back to Index