|
|
例如,下面的定理Involution on set with odd cardinality has fix point
证明只需要考虑轨道和奇偶性
又见math.stackexchange.com/questions/2926745/involution-on-set-with-odd-cardinality-fix-point
在Nuprl中的实现: nuprl.org/LibrarySnapshots/Published/Version2/Standard/equipolle ... on-has-fixpoint.html
Nuprl 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)))))
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)
|
|
