Theorem SimpleGraph.completeBipartiteGraph_isContained_iff

Modification history

2025-12-07 18:24

Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

feat(Combinatorics/SimpleGraph): characterise containment of `completeBipartiteGraph` (#27602) …

Added SimpleGraph.completeBipartiteGraph_isContained_iff View on Github →