PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
gen
1
1
1
1
1
1
1.
A:
Type
2.
B:
Type
3.
f:
A
B
4.
f1:
A
B
5.
g:
B
A
6.
InvFuns(A; B; f1; g)
7.
n:
8.
f2:
n
B
9.
g1:
B
n
10.
InvFuns(
n; B; f2; g1)
11.
Surj(A; B; f)
12.
b:
n
a:
n. (g1 o f o g o f2)(a) = b
By:
Unfold `surject` 11
THEN
Witness11 f2(b)
Generated subgoal:
1
11.
b:
n
12.
a:A. f(a) = f2(b)
a:
n. (g1 o f o g o f2)(a) = b
About:
n
a:A. f(a) = f2(b)
a:n. (g1 o f o g o f2)(a) = b
BBAnBnn; B; f2; g1)n a:n. (g1 o f o g o f2)(a) = bna:A. f(a) = f2(b) a:n. (g1 o f o g o f2)(a) = b
