---

Step * of Lemma fixedpoint-property-iff

No Annotations
∀X:Type. ∀d:metric(X).  (mcompact(X;d) ⇒ (FP(X) ⇐⇒ ∀f:FUN(X ⟶ X). (¬(∀x:X. f x # x))))
BY
{ Auto }

1
1. X : Type
2. d : metric(X)
3. mcompact(X;d)
4. FP(X)
5. f : FUN(X ⟶ X)
⊢ ¬(∀x:X. f x # x)

2
1. X : Type
2. d : metric(X)
3. mcompact(X;d)
4. ∀f:FUN(X ⟶ X). (¬(∀x:X. f x # x))
⊢ FP(X)

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:Type.  \mforall{}d:metric(X).    (mcompact(X;d)  {}\mRightarrow{}  (FP(X)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}f:FUN(X  {}\mrightarrow{}  X).  (\mneg{}(\mforall{}x:X.  f  x  \#  x))))


By

---

Latex:
Auto

---

Home Index