Nuprl

hbghlyj

例如,下面的定理

Involution on set with odd cardinality has fix point

证明只需要考虑轨道和奇偶性
又见math.stackexchange.com/questions/2926745/invo … ardinality-fix-point


在Nuprl中的实现: nuprl.org/LibrarySnapshots/Published/Version2 … 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)