---

Step * 2 of Lemma involution-has-fixpoint


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)
BY
{ ExRepD }

1
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
8. (∀o∈orbits.orbit(T;f;o))
9. ∀a:T. (∃o∈orbits. (a ∈ o))
10. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
11. no_repeats(T List;orbits)
12. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
⊢ ∃x:T. ((f x) = x ∈ T)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  [T]  :  Type
3.  T  \msim{}  \mBbbN{}n
4.  f  :  T  {}\mrightarrow{}  T
5.  \mforall{}x:T.  ((f  (f  x))  =  x)
6.  (n  rem  2)  =  1
7.  \mexists{}orbits:T  List  List
        ((\mforall{}o\mmember{}orbits.orbit(T;f;o))
        \mwedge{}  (\mforall{}a:T.  (\mexists{}o\mmember{}orbits.  (a  \mmember{}  o)))
        \mwedge{}  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
        \mwedge{}  no\_repeats(T  List;orbits)
        \mwedge{}  (n  =  l\_sum(map(\mlambda{}o.||o||;orbits))))
\mvdash{}  \mexists{}x:T.  ((f  x)  =  x)


By

---

Latex:
ExRepD

---

Home Index