Copy

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

Statistics

Metric	Count
Definitions Copy, bot, comp, id, induce, instFintypeOfSubtypeHomInjectiveCoe, instFunLike, isoSubgraphMap, isoToSubgraph, mapEdgeSet, mapNeighborSet, ofLE, toEmbedding, toHom, toSubgraph, topEmbedding, toCopy, toCopy, IsContained, IsIndContained, toCopy, coeCopy, copyCount, killCopies, instFintype, labelledCopyCount, «term_⊑_», «term_⊴_»	28
Theorems coe_comp, coe_id, coe_mk, coe_ofLE, coe_toHom, comp_apply, ext, ext_iff, injective, injective', instSubsingletonOfForall, ofLE_comp, ofLE_refl, range_toSubgraph, toHom_apply, toSubgraph_surjOn, topEmbedding_apply, congr_left, congr_right, killCopies_eq_left, bot, congr_left, congr_right, exists_iso_subgraph, mono_left, mono_right, of_exists_iso_subgraph, of_isEmpty, of_le, refl, rfl, trans, trans', trans_le, trans_le', compl, exists_iso_subgraph, isContained, of_compl, of_exists_iso_subgraph, of_isEmpty, refl, rfl, trans, isContained, isIndContained, isIndContained', isIndContained, coe_isContained, bot_isContained_iff_card_le, compl_isIndContained_compl, copyCount_bot, copyCount_eq_card_image_copyToSubgraph, copyCount_eq_zero, copyCount_le_labelledCopyCount, copyCount_of_isEmpty, copyCount_pos, free_bot, free_congr, free_congr_left, free_congr_right, free_killCopies, isContained_congr, isContained_congr_left, isContained_congr_right, isContained_iff_exists_iso_subgraph, isIndContained_iff_exists_iso_subgraph, killCopies_bot, killCopies_def, killCopies_eq_left, killCopies_le_left, labelledCopyCount_eq_zero, labelledCopyCount_of_isEmpty, labelledCopyCount_pos, le_card_edgeFinset_killCopies, le_card_edgeFinset_killCopies_add_copyCount, not_free, top_isIndContained_iff_top_isContained	78
Total	106

SimpleGraph

Definitions

Name	Category	Theorems
Copy 📖	CompData	14 math math: Copy.coe_mk, Copy.topEmbedding_apply, Copy.range_toSubgraph, Copy.toHom_apply, Copy.comp_apply, Copy.ext_iff, Copy.instSubsingletonOfForall, Copy.coe_id, isClique_range_copy_top, Copy.toSubgraph_surjOn, Copy.coe_ofLE, Copy.coe_comp, copyCount_eq_card_image_copyToSubgraph, Copy.coe_toHom
IsContained 📖	MathDef	30 math math: IsContained.of_extremalNumber_lt_card_edgeFinset, isContained_iff_exists_iso_subgraph, IsContained.trans, isContained_completeEquipartiteGraph_of_colorable, isContained_congr_right, IsContained.mono_left, IsContained.of_le, IsContained.congr_right, not_free, IsIndContained.isContained, top_isIndContained_iff_top_isContained, IsContained.refl, extremalNumber_of_fintypeCard_eq, IsContained.trans_le, IsContained.bot, bot_isContained_iff_card_le, IsContained.of_isEmpty, IsContained.trans_le', copyCount_pos, Iso.isContained, IsContained.rfl, completeBipartiteGraph_isContained_iff, isContained_congr, IsContained.mono_right, labelledCopyCount_pos, IsContained.congr_left, IsContained.of_exists_iso_subgraph, IsContained.trans', isContained_congr_left, Subgraph.coe_isContained
IsIndContained 📖	MathDef	13 math math: IsIndContained.trans, IsIndContained.rfl, Iso.isIndContained', IsIndContained.of_compl, IsIndContained.of_isEmpty, IsIndContained.of_exists_iso_subgraph, compl_isIndContained_compl, top_isIndContained_iff_top_isContained, IsIndContained.compl, isIndContained_iff_exists_iso_subgraph, Iso.isIndContained, IsIndContained.refl, Subgraph.IsInduced.isIndContained
copyCount 📖	CompOp	8 math math: copyCount_bot, le_card_edgeFinset_killCopies_add_copyCount, copyCount_pos, le_card_edgeFinset_killCopies, copyCount_eq_zero, copyCount_le_labelledCopyCount, copyCount_of_isEmpty, copyCount_eq_card_image_copyToSubgraph
killCopies 📖	CompOp	8 math math: killCopies_bot, killCopies_le_left, Free.killCopies_eq_left, le_card_edgeFinset_killCopies_add_copyCount, le_card_edgeFinset_killCopies, free_killCopies, killCopies_eq_left, killCopies_def
labelledCopyCount 📖	CompOp	4 math math: labelledCopyCount_eq_zero, copyCount_le_labelledCopyCount, labelledCopyCount_pos, labelledCopyCount_of_isEmpty
«term_⊑_» 📖	CompOp	—
«term_⊴_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_isContained_iff_card_le 📖	mathematical	—	IsContained Bot.bot SimpleGraph BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra Fintype.card	—	Fintype.card_le_of_embedding Function.Embedding.nonempty_of_card_le
compl_isIndContained_compl 📖	mathematical	—	IsIndContained Compl.compl SimpleGraph instCompl	—	Equiv.nonempty_congr
copyCount_bot 📖	mathematical	—	copyCount Bot.bot SimpleGraph BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra	—	copyCount.eq_1 Subgraph.ext set_fintype_card_eq_univ_iff Fintype.card_congr Subgraph.edge_vert Subgraph.Adj.symm RelIso.map_rel_iff Subgraph.Adj.coe Finset.card_singleton
copyCount_eq_card_image_copyToSubgraph 📖	mathematical	—	copyCount Finset.card Subgraph Finset.image Copy Copy.toSubgraph Finset.univ Copy.instFintypeOfSubtypeHomInjectiveCoe	—	copyCount.eq_1 Finset.coe_injective Finset.coe_filter Finset.coe_image Finset.coe_univ Set.image_univ Copy.range_toSubgraph
copyCount_eq_zero 📖	mathematical	—	copyCount Free	—	—
copyCount_le_labelledCopyCount 📖	mathematical	—	copyCount labelledCopyCount	—	copyCount_eq_card_image_copyToSubgraph Finset.card_image_le
copyCount_of_isEmpty 📖	mathematical	—	copyCount	—	nonempty_fintype Finite.of_subsingleton IsEmpty.instSubsingleton LE.le.antisymm LE.le.trans_eq copyCount_le_labelledCopyCount labelledCopyCount_of_isEmpty copyCount_pos IsContained.of_isEmpty
copyCount_pos 📖	mathematical	—	copyCount IsContained	—	—
free_bot 📖	mathematical	—	Free Bot.bot SimpleGraph BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra	—	edgeSet_nonempty Hom.map_mem_edgeSet edgeSet_bot Set.notMem_empty
free_congr 📖	mathematical	—	Free	—	Iff.not isContained_congr
free_congr_left 📖	mathematical	—	Free	—	free_congr
free_congr_right 📖	mathematical	—	Free	—	free_congr
free_killCopies 📖	mathematical	—	Free killCopies	—	deleteEdges.eq_1 Free.eq_1 isContained_iff_exists_iso_subgraph sdiff_le Subgraph.edgeSet_map Set.Nonempty.image Set.Nonempty.some_mem Iso.map_mem_edgeSet_iff Subgraph.edgeSet_subset Subgraph.edgeSet_coe edgeSet_sdiff edgeSet_fromEdgeSet edgeSet_sdiff_sdiff_isDiag Sym2.map_map Set.mem_singleton_iff Function.Injective.mem_set_image Equiv.Set.image_symm_apply Subgraph.image_coe_edgeSet_coe
isContained_congr 📖	mathematical	—	IsContained	—	IsContained.trans' IsContained.trans
isContained_congr_left 📖	mathematical	—	IsContained	—	isContained_congr
isContained_congr_right 📖	mathematical	—	IsContained	—	isContained_congr
isContained_iff_exists_iso_subgraph 📖	mathematical	—	IsContained Iso Set.Elem Subgraph.verts Subgraph.coe	—	IsContained.trans' Subgraph.coe_isContained
isIndContained_iff_exists_iso_subgraph 📖	mathematical	—	IsIndContained Subgraph.IsInduced	—	Set.image_congr Set.image_univ RelEmbedding.injective IsIndContained.trans Iso.isIndContained Subgraph.IsInduced.isIndContained
killCopies_bot 📖	mathematical	—	killCopies Bot.bot SimpleGraph BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra	—	killCopies_def
killCopies_def 📖	mathematical	—	killCopies SimpleGraph Bot.bot BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra deleteEdges Set.iUnion Sym2 Subgraph Iso Set.Elem Subgraph.verts Subgraph.coe Set Set.instSingletonSet Set.Nonempty.some Subgraph.edgeSet	—	—
killCopies_eq_left 📖	mathematical	—	killCopies Free	—	forall_swap Subgraph.edgeSet_subset
killCopies_le_left 📖	mathematical	—	SimpleGraph instLE killCopies	—	killCopies_def le_rfl deleteEdges_le
labelledCopyCount_eq_zero 📖	mathematical	—	labelledCopyCount Free	—	—
labelledCopyCount_of_isEmpty 📖	mathematical	—	labelledCopyCount	—	Fintype.card_unique Copy.instSubsingletonOfForall Unique.instSubsingleton
labelledCopyCount_pos 📖	mathematical	—	labelledCopyCount IsContained	—	—
le_card_edgeFinset_killCopies 📖	mathematical	—	Finset.card Sym2 edgeFinset copyCount killCopies killCopies.edgeSet.instFintype	—	eq_or_ne Fintype.card_congr' killCopies_bot Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Set.toFinset_card edgeFinset.eq_1 copyCount.eq_1 Finset.card_subtype Finset.subtype_univ Finset.card_univ Finset.card_image_le Set.toFinset_range Finset.le_card_sdiff Set.toFinset_congr edgeSet_deleteEdges Set.iUnion_subtype Set.iUnion_congr_Prop Finset.sdiff_eq_inter_compl Finset.coe_inter Set.coe_toFinset Finset.coe_compl Set.compl_iUnion Fintype.card_ofFinset Finset.coe_filter
le_card_edgeFinset_killCopies_add_copyCount 📖	mathematical	—	Finset.card Sym2 edgeFinset killCopies killCopies.edgeSet.instFintype copyCount	—	tsub_le_iff_right Nat.instOrderedSub le_card_edgeFinset_killCopies
not_free 📖	mathematical	—	Free IsContained	—	—
top_isIndContained_iff_top_isContained 📖	mathematical	—	IsIndContained Top.top SimpleGraph BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra IsContained	—	IsIndContained.isContained

SimpleGraph.Copy

Definitions

Name	Category	Theorems
bot 📖	CompOp	—
comp 📖	CompOp	3 math math: comp_apply, ofLE_comp, coe_comp
id 📖	CompOp	2 math math: coe_id, ofLE_refl
induce 📖	CompOp	—
instFintypeOfSubtypeHomInjectiveCoe 📖	CompOp	1 math math: SimpleGraph.copyCount_eq_card_image_copyToSubgraph
instFunLike 📖	CompOp	10 math math: coe_mk, topEmbedding_apply, toHom_apply, comp_apply, ext_iff, coe_id, SimpleGraph.isClique_range_copy_top, coe_ofLE, coe_comp, coe_toHom
isoSubgraphMap 📖	CompOp	—
isoToSubgraph 📖	CompOp	—
mapEdgeSet 📖	CompOp	—
mapNeighborSet 📖	CompOp	—
ofLE 📖	CompOp	3 math math: ofLE_refl, coe_ofLE, ofLE_comp
toEmbedding 📖	CompOp	4 math math: SimpleGraph.UnitDistEmbedding.iso_p_apply, SimpleGraph.UnitDistEmbedding.embed_p_apply, SimpleGraph.isNClique_map_copy_top, SimpleGraph.UnitDistEmbedding.copy_p_apply
toHom 📖	CompOp	4 math math: toHom_apply, injective, injective', coe_toHom
toSubgraph 📖	CompOp	3 math math: range_toSubgraph, toSubgraph_surjOn, SimpleGraph.copyCount_eq_card_image_copyToSubgraph
topEmbedding 📖	CompOp	1 math math: topEmbedding_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe SimpleGraph.Copy instFunLike comp	—	comp_apply
coe_id 📖	mathematical	—	DFunLike.coe SimpleGraph.Copy instFunLike id	—	—
coe_mk 📖	mathematical	DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	SimpleGraph.Copy instFunLike	—	—
coe_ofLE 📖	mathematical	SimpleGraph SimpleGraph.instLE	DFunLike.coe SimpleGraph.Copy instFunLike ofLE	—	—
coe_toHom 📖	mathematical	—	DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj toHom SimpleGraph.Copy instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe SimpleGraph.Copy instFunLike comp	—	RelHom.comp_apply
ext 📖	—	DFunLike.coe SimpleGraph.Copy instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe SimpleGraph.Copy instFunLike	—	ext
injective 📖	mathematical	—	DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj toHom	—	injective'
injective' 📖	mathematical	—	DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj toHom	—	—
instSubsingletonOfForall 📖	mathematical	—	SimpleGraph.Copy	—	Function.Injective.subsingleton DFunLike.coe_injective
ofLE_comp 📖	mathematical	SimpleGraph SimpleGraph.instLE	comp ofLE LE.le.trans PartialOrder.toPreorder SimpleGraph.instPartialOrder	—	ext LE.le.trans comp_apply
ofLE_refl 📖	mathematical	—	ofLE le_rfl SimpleGraph PartialOrder.toPreorder SimpleGraph.instPartialOrder id	—	ext le_rfl
range_toSubgraph 📖	mathematical	—	Set.range SimpleGraph.Subgraph SimpleGraph.Copy toSubgraph setOf SimpleGraph.Iso Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	—	Set.ext SimpleGraph.Subgraph.hom_injective RelIso.injective SimpleGraph.Subgraph.map_comp SimpleGraph.Subgraph.map_iso_top SimpleGraph.Subgraph.map_hom_top
toHom_apply 📖	mathematical	—	DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj toHom SimpleGraph.Copy instFunLike	—	—
toSubgraph_surjOn 📖	mathematical	—	Set.SurjOn SimpleGraph.Copy SimpleGraph.Subgraph toSubgraph Set.univ setOf SimpleGraph.Iso Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	—	Set.image_univ range_toSubgraph
topEmbedding_apply 📖	mathematical	—	DFunLike.coe RelEmbedding SimpleGraph.Adj Top.top SimpleGraph BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra SimpleGraph.completeAtomicBooleanAlgebra RelEmbedding.instFunLike topEmbedding SimpleGraph.Copy instFunLike	—	—

SimpleGraph.Embedding

Definitions

Name	Category	Theorems
toCopy 📖	CompOp	1 math math: SimpleGraph.UnitDistEmbedding.embed_p_apply

SimpleGraph.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_left 📖	—	SimpleGraph.Free	—	—	SimpleGraph.free_congr_left
congr_right 📖	—	SimpleGraph.Free	—	—	SimpleGraph.free_congr_right
killCopies_eq_left 📖	mathematical	SimpleGraph.Free	SimpleGraph.killCopies	—	eq_or_ne SimpleGraph.killCopies_bot SimpleGraph.killCopies_eq_left

SimpleGraph.Hom

Definitions

Name	Category	Theorems
toCopy 📖	CompOp	—

SimpleGraph.IsContained

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot 📖	mathematical	—	SimpleGraph.IsContained Bot.bot SimpleGraph BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra SimpleGraph.completeAtomicBooleanAlgebra Fintype.card	—	SimpleGraph.bot_isContained_iff_card_le
congr_left 📖	mathematical	—	SimpleGraph.IsContained	—	SimpleGraph.isContained_congr_left
congr_right 📖	mathematical	—	SimpleGraph.IsContained	—	SimpleGraph.isContained_congr_right
exists_iso_subgraph 📖	mathematical	—	SimpleGraph.Iso Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	—	SimpleGraph.isContained_iff_exists_iso_subgraph
mono_left 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.IsContained	—	trans of_le
mono_right 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.IsContained	—	trans of_le
of_exists_iso_subgraph 📖	mathematical	SimpleGraph.Iso Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	SimpleGraph.IsContained	—	SimpleGraph.isContained_iff_exists_iso_subgraph
of_isEmpty 📖	mathematical	—	SimpleGraph.IsContained	—	—
of_le 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.IsContained	—	—
refl 📖	mathematical	—	SimpleGraph.IsContained	—	—
rfl 📖	mathematical	—	SimpleGraph.IsContained	—	refl
trans 📖	mathematical	—	SimpleGraph.IsContained	—	—
trans' 📖	mathematical	—	SimpleGraph.IsContained	—	trans
trans_le 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.IsContained	—	mono_right
trans_le' 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.IsContained	—	mono_left

SimpleGraph.IsIndContained

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	—	SimpleGraph.IsIndContained Compl.compl SimpleGraph SimpleGraph.instCompl	—	SimpleGraph.compl_isIndContained_compl
exists_iso_subgraph 📖	mathematical	—	SimpleGraph.Subgraph.IsInduced	—	SimpleGraph.isIndContained_iff_exists_iso_subgraph
isContained 📖	mathematical	—	SimpleGraph.IsContained	—	—
of_compl 📖	mathematical	—	SimpleGraph.IsIndContained	—	SimpleGraph.compl_isIndContained_compl
of_exists_iso_subgraph 📖	mathematical	SimpleGraph.Subgraph.IsInduced	SimpleGraph.IsIndContained	—	SimpleGraph.isIndContained_iff_exists_iso_subgraph
of_isEmpty 📖	mathematical	—	SimpleGraph.IsIndContained	—	—
refl 📖	mathematical	—	SimpleGraph.IsIndContained	—	—
rfl 📖	mathematical	—	SimpleGraph.IsIndContained	—	refl
trans 📖	mathematical	—	SimpleGraph.IsIndContained	—	—

SimpleGraph.Iso

Definitions

Name	Category	Theorems
toCopy 📖	CompOp	1 math math: SimpleGraph.UnitDistEmbedding.iso_p_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isContained 📖	mathematical	—	SimpleGraph.IsContained	—	—
isIndContained 📖	mathematical	—	SimpleGraph.IsIndContained	—	—
isIndContained' 📖	mathematical	—	SimpleGraph.IsIndContained	—	isIndContained

SimpleGraph.Subgraph

Definitions

Name	Category	Theorems
coeCopy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_isContained 📖	mathematical	—	SimpleGraph.IsContained Set.Elem verts coe	—	—

SimpleGraph.Subgraph.IsInduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIndContained 📖	mathematical	SimpleGraph.Subgraph.IsInduced	SimpleGraph.IsIndContained Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	—	Subtype.coe_injective adj

SimpleGraph.killCopies.edgeSet

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	2 math math: SimpleGraph.le_card_edgeFinset_killCopies_add_copyCount, SimpleGraph.le_card_edgeFinset_killCopies

---

← Back to Index