Step
*
1
1
of Lemma
fixedpoint-property-iff
1. X : Type
2. d : metric(X)
3. mcompact(X;d)
4. f : FUN(X ⟶ X)
5. ∀n:ℕ+. ∃x:X. (mdist(d;f x;x) ≤ (r1/r(n)))
⊢ ¬(∀x:X. f x # x)
BY
{ ((D 0 THENA Auto) THEN RepUR ``msep`` -1) }
1
1. X : Type
2. d : metric(X)
3. mcompact(X;d)
4. f : FUN(X ⟶ X)
5. ∀n:ℕ+. ∃x:X. (mdist(d;f x;x) ≤ (r1/r(n)))
6. ∀x:X. (r0 < mdist(d;f x;x))
⊢ False
Latex:
Latex:
1. X : Type
2. d : metric(X)
3. mcompact(X;d)
4. f : FUN(X {}\mrightarrow{} X)
5. \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}x:X. (mdist(d;f x;x) \mleq{} (r1/r(n)))
\mvdash{} \mneg{}(\mforall{}x:X. f x \# x)
By
Latex:
((D 0 THENA Auto) THEN RepUR ``msep`` -1)
Home
Index