Metamath Proof Explorer
Table of Contents - 17.1.2.3. The vertices and edges of a graph represented as extensible structure
- funvtxdmge2val
- funiedgdmge2val
- funvtxdm2val
- funiedgdm2val
- funvtxval0
- basvtxval
- edgfiedgval
- funvtxval
- funiedgval
- structvtxvallem
- structvtxval
- structiedg0val
- structgrssvtxlem
- structgrssvtx
- structgrssiedg
- struct2grstr
- struct2grvtx
- struct2griedg
- graop
- grastruct
- gropd
- grstructd
- gropeld
- grstructeld
- setsvtx
- setsiedg