feat(Combinatorics/SimpleGraph): Konig’s theorem on bipartite graphs

[ksenono]

---

[github-actions[bot]]

PR summary 262278786e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.VertexCover (new file)	609
Mathlib.Combinatorics.SimpleGraph.Konig.Auxillary (new file)	813
Mathlib.Combinatorics.SimpleGraph.Konig.KonigFin (new file)	815
Mathlib.Combinatorics.SimpleGraph.Konig.Konig (new file)	816

---

Declarations diff

+ HomClass + IsMatching.dart_card_eq_vert_card + IsMatching.edge_card_eq_double_vert_card + IsMatching.iSup_of_isChain + IsMatching.matching_restricted + IsMinimalCover + IsVertexCover + IsVertexCover.mono + IsVertexCover.preimage + IsVertexCover.subset + IsVertexCover.vertexCoverNum_le + Subgraph.IsMaxSizeMatching + Subgraph.IsMaximalMatching + add_lt_add_iff_of_lt_aleph0 + add_lt_add_of_lt_of_lt + card_darts + card_lt_fin_card + card_upcast_edgeSet + disjoint_verts_iff_disjoint + eq_bot_iff_forall_not_adj + eq_top_iff_exists_not_adj + exists_isMaximalMatching + exists_of_le_vertexCoverNum + fin_card_lt_card + finite_min_size_cover_minimal + hall_condition + hall_wrapper + isBipartite.subgraph + isBipartiteWith_subgraph + isClique_iff_isChain_adj + isIndepSet_compl_iff_isVertexCover + isIndepSet_iff_isAntichain + isIndepSet_iff_isAntichain_adj + isMatching.of_connected_pair + isVertexCover_bot + isVertexCover_compl + isVertexCover_empty + isVertexCover_image_iso + isVertexCover_preimage_iso + isVertexCover_univ + konig_finite_matching + konig_infinite_cover + maximal_matching_is_cover + min_size_cover_exists + minimal_cover_no_isolated + mul_nat_cancel_iff + mul_nat_le_mul_nat + mul_nat_lt_mul_nat + mul_nat_strictMono + nat_mul_cancel_iff + nat_mul_le_nat_mul + nat_mul_lt_nat_mul + nat_mul_strictMono + restricted_max_matching + subgraph_upcast + upcast_matching + vertexCoverNum + vertexCoverNum_bot + vertexCoverNum_congr + vertexCoverNum_eq_zero + vertexCoverNum_exists + vertexCoverNum_le_card_sub_one + vertexCoverNum_le_encard_edgeSet + vertexCoverNum_le_iff + vertexCoverNum_le_vertexCoverNum_of_injective + vertexCoverNum_lt_card + vertexCoverNum_mono + vertexCoverNum_ne_top_of_finite + vertexCoverNum_ne_top_of_finite_edgeSet + vertexCoverNum_of_subsingleton + vertexCoverNum_top ++ IsMinSizeCover

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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#30129
• leanprover-community/mathlib4#32552
• leanprover-community/mathlib4#32555
• leanprover-community/mathlib4#32570 By Dependent Issues (🤖). Happy coding!

[vlad902]

I'll repost this comment since I'm not sure if you've seen it: mathlib generally wants maximum generality for the results it includes. I am not familiar with the proof of Konig-Egervary, is the proof of Konig's theorem a component of the weighted-graph version? Is it possible to extend your argument to weighted graphs (e.g. using https://github.com/leanprover-community/mathlib4/pull/30047) and derive this as a corollary instead? Without knowing the specifics of the proofs, I'd argue that is the correct generality.

I'll also note that I'm not a mathlib maintainer/reviewer, so don't take my opinion on the correct generality as truth.

[vlad902]

Also, I have not deeply looked at the argument to see whether it makes sense, but: you are directly using the combinatorial Hall's marriage theorem--have you seen that there is already an analogous version proved for bipartite graphs? I wasn't sure if you had not seen it or if it was not suitable for this application.

[ksenono]

I'll repost this comment since I'm not sure if you've seen it: mathlib generally wants maximum generality for the results it includes. I am not familiar with the proof of Konig-Egervary, is the proof of Konig's theorem a component of the weighted-graph version? Is it possible to extend your argument to weighted graphs (e.g. using #30047) and derive this as a corollary instead? Without knowing the specifics of the proofs, I'd argue that is the correct generality.

I'll also note that I'm not a mathlib maintainer/reviewer, so don't take my opinion on the correct generality as truth.

Thanks — I did miss your comment on the previous PR!

I initially considered presenting Egérváry’s theorem as a generalization of Kőnig’s theorem for finite graphs, but I instead opted for a version of Kőnig’s theorem for potentially infinite/uncountable graphs, which isn’t compatible with Egérváry’s theorem.

Moreover, this version also yields a short proof of Dilworth’s theorem. However, I think I can prove Egérváry’s theorem in a separate PR.