(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: inverse-biject 1 1
1. A: Type
2. B: Type
3. f: AB
4. Bij(A; B; f)
5. g: BA
6. InvFuns(A; B; f; g)
7. InvFuns(B; A; g; f)
Bij(B; A; g)
By: Inst Thm* f:(AB), g:(BA). InvFuns(A; B; f; g) Bij(A; B; f) [B;A;g;f]
Generated subgoals:

None

About:
functionuniverseimpliesall

(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc