---

Step * of Lemma rng_prod_injection

No Annotations
∀[r:CRng]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|]. ∀[f:ℕn →⟶ ℕn].  ((Π(r) 0 ≤ i < n. F[i]) = (Π(r) 0 ≤ i < n. F[f i]) ∈ |r|)
BY
{ (Auto
   THEN ((InstLemma `permutation-generators4` [⌜n⌝;⌜λ2f.(Π(r) 0 ≤ i < n. F[i]) = (Π(r) 0 ≤ i < n. F[f i]) ∈ |r|⌝]⋅
         THENM (BHyp -1 THEN Auto)
         )
         THENA (Auto THEN Reduce 0 THEN Auto THEN (Thin 4 THEN RenameVar `f' 4) THEN NthHypEqTrans (-1))
         )
   ) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. F : ℕn ⟶ |r|
4. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} @i
5. j : ℕ+n@i
6. (Π(r) 0 ≤ i < n. F[i]) = (Π(r) 0 ≤ i < n. F[f i]) ∈ |r|
⊢ (Π(r) 0 ≤ i < n. F[f i]) = (Π(r) 0 ≤ i < n. F[f ((0, j) i)]) ∈ |r|

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  {}\mrightarrow{}  |r|].  \mforall{}[f:\mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n].
    ((\mPi{}(r)  0  \mleq{}  i  <  n.  F[i])  =  (\mPi{}(r)  0  \mleq{}  i  <  n.  F[f  i]))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `permutation-generators4`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.(\mPi{}(r)  0 
                                                                                                                        \mleq{}  i 
                                                                                                                        <  n
                                                                                                                F[i])
                                                                                                    =  (\mPi{}(r)  0 
                                                                                                                    \mleq{}  i 
                                                                                                                    <  n
                                                                                                            F[f  i])\mkleeneclose{}]\mcdot{}
              THENM  (BHyp  -1  THEN  Auto)
              )
              THENA  (Auto
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (Thin  4  THEN  RenameVar  `f'  4)
                            THEN  NthHypEqTrans  (-1))
              )
  )

---

Home Index