Nuprl - Proof: nsub surj least preimage works gen 1

(12steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub surj least preimage works gen 1

1. B : Type
2. e : B

B

3. IsEqFun(B;e)
4. a :

5. f :

a onto

B
6. y : B

f(least x:

. (f(x)) e y) = y

By:	((x.(f(x)) e y) {p:(a)\| i:a. p(i) } Asserted (THEN ((Use:[a \| p(x):= (f(x)) e y] ((Inst: Thm* k:, p:{p:(k)\| i:k. p(i) }. p(least i:. p(i)))) THEN Analyze5

Generated subgoals:

1 5. f : aB
6. Surj(a; B; f)
7. y : B
  (x.(f(x)) e y)  {p:(a)| i:a. p(i) }
4 steps

2 5. f : aB
6. Surj(a; B; f)
7. y : B
8. (x.(f(x)) e y)  {p:(a)| i:a. p(i) }
9. (f(least i:. (f(i)) e y)) e y
  f(least x:. (f(x)) e y) = y
6 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(12steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc