Nuprl - Proof: nsub inj discr range bij

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj discr range bij

A:Type.

(A Discrete)

(

k:

, f:(

k inj

A).

({a:A|

i:

k. a = f(i) }

Type

(& f

k

{a:A|

i:

k. a = f(i) }

(& Bij(

k; {a:A|

i:

k. a = f(i) }; f))

By:	SimilarTo Thm* (A Discrete) Thm* Thm* (k:, f:(kA). Thm* ({a:A\| i:k. a = f(i) } Type Thm* (& f k{a:A\| i:k. a = f(i) } Thm* (& Surj(k; {a:A\| i:k. a = f(i) }; f))

Generated subgoal:

1 1. A : Type
2. A Discrete
3. k :
4. f:(kA).
4. {a:A| i:k. a = f(i) }  Type
4. & f  k{a:A| i:k. a = f(i) }
4. & Surj(k; {a:A| i:k. a = f(i) }; f)
  f:(k inj A).
  {a:A| i:k. a = f(i) }  Type
  & f  k{a:A| i:k. a = f(i) }
  & Bij(k; {a:A| i:k. a = f(i) }; f)
5 steps

About:

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

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