Metamath Proof Explorer
Table of Contents - 16.2.3. Loop-free graphs
For a hypergraph, the property to be "loop-free" is expressed by
with and
. is the set of edges which connect at least two
vertices.
- umgrislfupgrlem
- umgrislfupgr
- lfgredgge2
- lfgrnloop