Step * 1 2 1 of Lemma permutation_inversion


1. [A] Type
2. as List
3. bs List
4. : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs (as f) ∈ (A List)
7. ||as|| ||bs|| ∈ ℤ
8. : ℕ||as|| ⟶ ℕ||as||
9. ∀x:ℕ||as||. ((f (g x)) x ∈ ℤ)
⊢ Inj(ℕ||as||;ℕ||as||;g)
BY
(D THEN Auto) }

1
1. Type
2. as List
3. bs List
4. : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs (as f) ∈ (A List)
7. ||as|| ||bs|| ∈ ℤ
8. : ℕ||as|| ⟶ ℕ||as||
9. ∀x:ℕ||as||. ((f (g x)) x ∈ ℤ)
10. a1 : ℕ||as||
11. a2 : ℕ||as||
12. (g a1) (g a2) ∈ ℕ||as||
⊢ a1 a2 ∈ ℕ||as||


Latex:


Latex:

1.  [A]  :  Type
2.  as  :  A  List
3.  bs  :  A  List
4.  f  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
5.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)
6.  bs  =  (as  o  f)
7.  ||as||  =  ||bs||
8.  g  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
9.  \mforall{}x:\mBbbN{}||as||.  ((f  (g  x))  =  x)
\mvdash{}  Inj(\mBbbN{}||as||;\mBbbN{}||as||;g)


By


Latex:
(D  0  THEN  Auto)




Home Index