finite
sets
Sections
AutomataTheory
Doc
inject
Def
basic Inj(A;B;f) ==
a1,a2:A. f(a1) = f(a2)
B
a1 = a2
Thm*
f:(A
B). Inj(A;B;f)
Prop
a1,a2:A. f(a1) = f(a2) 
B 
a1 = a2
f:(A
B). Inj(A;B;f) Prop