[Merged by Bors] - feat(Combinatorics/SimpleGraph): define Copy

[mitchell-horner]

Define the type Copy as the subtype of injective homomorphisms.

Also define

• the predicate that a simple graph contains another simple graph IsContained (equivalent to "is isomorphic to a subgraph of"),
• the predicate that a simple graph is free of another simple graph Free for convenience.

---

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[YaelDillies]

Can you merge master? This will fix the bot

[kbuzzard]

@mitchell-horner can you merge master and resolve all comments which you have dealt with?

[github-actions]

PR summary ea7425d09e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Copy (new file)	593

---

Declarations diff

+ Copy
+ Embedding.toCopy
+ Free
+ Hom.toCopy
+ IsContained
+ IsContained.bot
+ IsContained.exists_iso_subgraph
+ IsContained.mono_left
+ IsContained.mono_right
+ IsContained.of_exists_iso_subgraph
+ IsContained.of_isEmpty
+ IsContained.of_le
+ IsContained.refl
+ IsContained.rfl
+ IsContained.trans
+ IsContained.trans'
+ IsContained.trans_le
+ IsContained.trans_le'
+ Iso.toCopy
+ Subgraph.Copy.map
+ Subgraph.coeCopy
+ Subgraph.coe_isContained
+ bot
+ bot_isContained_iff_card_le
+ coe_comp
+ coe_id
+ coe_ofLE
+ coe_toHom
+ coe_toHom_apply
+ comp
+ comp_apply
+ free_bot
+ free_congr
+ id
+ induce
+ injective
+ instance : FunLike (Copy A B) α β
+ isContained_congr
+ isContained_iff_exists_iso_subgraph
+ mapEdgeSet
+ mapNeighborSet
+ not_free
+ ofLE
+ ofLE_comp
+ ofLE_refl
+ toEmbedding
+ toHom

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mitchell-horner]

@kbuzzard I've been waiting for others' input on the name SubgraphIso. Feel free to weigh in. 😁

[YaelDillies]

I still think IsContained is a better name than IsIsoSubgraph. What do you think, @b-mehta ?

[YaelDillies]

Thanks!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[b-mehta]

Thanks!

bors d+

[mathlib-bors]

✌️ mitchell-horner can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mitchell-horner]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style