---

Step * of Lemma finite-injection

No Annotations
∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀n:ℕ. ∀s:ℕn ⟶ T.  (Surj(ℕn;T;s) ⇒ (∀f:T ⟶ T. ∀x:T. ∃m:ℕ+n + 1. ((f^m x) = x ∈ T) supposing Inj(T;T;f)))))
BY
{ (Auto THEN (FLemma `surject-inverse` [5] THENA Auto) THEN D -1) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. n : ℕ
4. s : ℕn ⟶ T
5. Surj(ℕn;T;s)
6. f : T ⟶ T
7. Inj(T;T;f)
8. x : T
9. g : T ⟶ ℕn
10. ∀x:T. ((s (g x)) = x ∈ T)
⊢ ∃m:ℕ+n + 1. ((f^m x) = x ∈ T)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
                (Surj(\mBbbN{}n;T;s)  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x:T.  \mexists{}m:\mBbbN{}\msupplus{}n  +  1.  ((f\^{}m  x)  =  x)  supposing  Inj(T;T;f)))))


By

---

Latex:
(Auto  THEN  (FLemma  `surject-inverse`  [5]  THENA  Auto)  THEN  D  -1)

---

Home Index