Commit 2025-03-17 19:45 2fd915dd

View on Github →

feat: the image of a subgraph under its embedding is itself (#22955) From ExtrProbCombi (LeanCamCombi)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

modified def SimpleGraph.Subgraph.coeCopy

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.comap_equiv_top

deleted theorem SimpleGraph.Subgraph.hom.injective

added theorem SimpleGraph.Subgraph.hom_injective

added theorem SimpleGraph.Subgraph.map_hom_top

added theorem SimpleGraph.Subgraph.map_iso_top

deleted theorem SimpleGraph.Subgraph.spanningHom.injective

added theorem SimpleGraph.Subgraph.spanningHom_injective