Theorem Hypergraph.sUnion_edgeSet_eq_vertexSet_iff_all_vertex_not_isolated

Modification history

2026-06-12 00:00
Mathlib/Combinatorics/Hypergraph/Basic.lean
feat(Combinatorics): define undirected hypergraphs (#28613) …
Added Hypergraph.sUnion_edgeSet_eq_vertexSet_iff_all_vertex_not_isolatedView on Github →