(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Composing bijections gives a bijection.

At: comp preserves bij

  A,B,C:Type, g:(AB), f:(BC).
  Bij(A; B; g)  Bij(B; C; f)  Bij(A; C; f o g)
By: Def of Bij(<A>; <B>; <f>) THEN UnivCD

Generated subgoal:

1 1. A : Type
2. B : Type
3. C : Type
4. g : AB
5. f : BC
6. Inj(A; B; g) & Surj(A; B; g)
7. Inj(B; C; f) & Surj(B; C; f)
  Inj(A; C; f o g) & Surj(A; C; f o g)
1 step

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

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