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`, `instTransIsContained`, `instTransIsIndContained`, `killCopies`, `instFintype`, `labelledCopyCount`, `«term_⊑_»`, `«term_⊴_»`	30
Theorems `coe_comp`, `coe_id`, `coe_mk`, `coe_ofLE`, `coe_toHom`, `comp_apply`, `degree_le`, `ext`, `ext_iff`, `injective`, `injective'`, `instSubsingletonOfForall`, `max_degree_le`, `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`, `max_degree_le`, `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`, `instIsPreorderIsContained`, `instIsPreorderIsIndContained`, `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`	83
Total	113

SimpleGraph

Definitions

Name	Category	Theorems
`Copy` 📖	CompData	15 math math: `Copy.coe_mk`, `Copy.topEmbedding_apply`, `Copy.range_toSubgraph`, `Copy.toHom_apply`, `Copy.comp_apply`, `Copy.ext_iff`, `Copy.degree_le`, `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	37 math math: `IsContained.of_extremalNumber_lt_card_edgeFinset`, `completeEquipartiteGraph_isContained_iff`, `isContained_iff_exists_iso_subgraph`, `IsContained.trans`, `isContained_completeEquipartiteGraph_of_colorable`, `completeBipartiteGraph_isContained_bipartiteDoubleCover`, `isContained_congr_right`, `IsContained.mono_left`, `IsContained.of_le`, `IsContained.congr_right`, `instIsPreorderIsContained`, `not_free`, `completeEquipartiteGraph_succ_isContained_iff`, `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.lineGraph`, `IsContained.rfl`, `isContained_of_card_edgeFinset`, `completeBipartiteGraph_isContained_iff`, `isContained_congr`, `Walk.IsPath.isContained_pathGraph`, `IsContained.mono_right`, `labelledCopyCount_pos`, `IsContained.congr_left`, `IsContained.of_exists_iso_subgraph`, `IsContained.trans'`, `isContained_congr_left`, `Subgraph.coe_isContained`
`IsIndContained` 📖	MathDef	16 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`, `IsContained.isIndContained_lineGraph`, `IsIndContained.lineGraph`, `instIsPreorderIsIndContained`, `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`
`instTransIsContained` 📖	CompOp	—
`instTransIsIndContained` 📖	CompOp	—
`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`
`instIsPreorderIsContained` 📖	mathematical	—	`IsPreorder` `SimpleGraph` `IsContained`	—	`IsContained.refl` `IsContained.trans`
`instIsPreorderIsIndContained` 📖	mathematical	—	`IsPreorder` `SimpleGraph` `IsIndContained`	—	`IsIndContained.refl` `IsIndContained.trans`
`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` `Subgraph` `Iso` `Set.Elem` `Subgraph.verts` `Subgraph.coe`	—	`IsContained.trans'` `Subgraph.coe_isContained`
`isIndContained_iff_exists_iso_subgraph` 📖	mathematical	—	`IsIndContained` `Subgraph` `Iso` `Set.Elem` `Subgraph.verts` `Subgraph.coe` `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`	—	`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` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `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` `Finset.ext` `Sym2.inductionOn` `edgeSet_deleteEdges`
`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	11 math math: `coe_mk`, `topEmbedding_apply`, `toHom_apply`, `comp_apply`, `ext_iff`, `degree_le`, `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`	`DFunLike.coe` `SimpleGraph.Copy` `instFunLike` `SimpleGraph.Hom` `RelHom.instFunLike` `SimpleGraph.Adj`	—	—
`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`
`degree_le` 📖	mathematical	—	`SimpleGraph.degree` `DFunLike.coe` `SimpleGraph.Copy` `instFunLike`	—	`SimpleGraph.card_neighborSet_eq_degree` `Fintype.card_le_of_injective` `Function.Embedding.injective`
`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`
`max_degree_le` 📖	mathematical	—	`SimpleGraph.maxDegree`	—	`isEmpty_or_nonempty` `SimpleGraph.maxDegree_of_isEmpty` `Nat.instCanonicallyOrderedAdd` `SimpleGraph.exists_maximal_degree_vertex`
`ofLE_comp` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`comp` `ofLE` `LE.le.trans` `SimpleGraph` `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` 📖	mathematical	`SimpleGraph.Free`	`SimpleGraph.Free`	—	`SimpleGraph.free_congr_left`
`congr_right` 📖	mathematical	`SimpleGraph.Free`	`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.Subgraph` `SimpleGraph.Iso` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe`	—	`SimpleGraph.isContained_iff_exists_iso_subgraph`
`max_degree_le` 📖	mathematical	—	`SimpleGraph.maxDegree`	—	`SimpleGraph.Copy.max_degree_le`
`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.Subgraph` `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` `SimpleGraph.Iso` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe` `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` `SimpleGraph.Iso` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe` `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