Thms finite sets Sections AutomataTheory Doc

biject Def Bij(A;B;f) == Inj(A;B;f) & Surj(A;B;f)

Thm* f:(AB). Bij(A;B;f) Prop

surject Def Surj(A;B;f) == b:B. a:A. f(a) = b

Thm* f:(AB). Surj(A;B;f) Prop

inject Def basic Inj(A;B;f) == a1,a2:A. f(a1) = f(a2) B a1 = a2

Thm* f:(AB). Inj(A;B;f) Prop