f:(A
BA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) 
b1 = b2) (a,a':A. Dec(
b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) 
Graph(a,a':A. b:B. a' = f(a,b))
-- > i
n | n:)
B, incidence = 
< a,b > . < a,f(a;b) > >
is mentioned by
| Thm* f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b)) | [fun-graph-rel-graph] |
| Def DivGraph_2 == Graph(i: -- > in | n:) | [divides-graph2] |
Try larger context:
Graphs