det
automata
Sections
AutomataTheory
Doc
surject
Def
Surj(A; B; f) ==
b:B.
a:A. f(a) = b
Thm*
A,B:Type, f:(A
B). Surj(A; B; f)
Prop
About:
b:B. 
a:A. f(a) = b
A,B:Type, f:(A
B). Surj(A; B; f) 
Propb:B. a:A. f(a) = b
