---

Step * of Lemma involution-has-fixpoint

∀n:ℕ
  ∀[T:Type]. (T ~ ℕn ⇒ (∀f:T ⟶ T. ((∀x:T. ((f (f x)) = x ∈ T)) ⇒ ((n rem 2) = 1 ∈ ℤ) ⇒ (∃x:T. ((f x) = x ∈ T)))))
BY
{ (Intros THEN (InstLemma `count-by-orbits` [⌜n⌝;⌜T⌝;⌜f⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. n : ℕ
2. T : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. (n rem 2) = 1 ∈ ℤ
⊢ Inj(T;T;f)

2
1. n : ℕ
2. [T] : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. (n rem 2) = 1 ∈ ℤ
7. ∃orbits:T List List
    ((∀o∈orbits.orbit(T;f;o))
    ∧ (∀a:T. (∃o∈orbits. (a ∈ o)))
    ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
    ∧ no_repeats(T List;orbits)
    ∧ (n = l_sum(map(λo.||o||;orbits)) ∈ ℤ))
⊢ ∃x:T. ((f x) = x ∈ T)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[T:Type]
        (T  \msim{}  \mBbbN{}n  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  ((\mforall{}x:T.  ((f  (f  x))  =  x))  {}\mRightarrow{}  ((n  rem  2)  =  1)  {}\mRightarrow{}  (\mexists{}x:T.  ((f  x)  =  x)))))


By

---

Latex:
(Intros  THEN  (InstLemma  `count-by-orbits`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index