Commit 2026-01-07 14:25 d5cad8f7

View on Github →

refactor(Combinatorics/SimpleGraph/VertexCover): assumes containment instead of injective hom (#33622) Follow-up to this PR comment

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

Modified Mathlib/Combinatorics/SimpleGraph/VertexCover.lean

added theorem SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum

deleted theorem SimpleGraph.vertexCoverNum_le_vertexCoverNum_of_injective