---

Step * 3 1 1 of Lemma topfuneq-equiv


1. X : Space
2. Y : Space
3. Sym(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
4. a : topfun(X;Y)
5. b : topfun(X;Y)
6. c : topfun(X;Y)
7. ∀x:|X|. topeq(Y;b x;c x)
8. x : |X|
9. topeq(Y;b x;c x)
10. topeq(Y;a x;b x)
⊢ topeq(Y;a x;c x)
BY
{ (FLemma `topeq_transitivity` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Space
2.  Y  :  Space
3.  Sym(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
4.  a  :  topfun(X;Y)
5.  b  :  topfun(X;Y)
6.  c  :  topfun(X;Y)
7.  \mforall{}x:|X|.  topeq(Y;b  x;c  x)
8.  x  :  |X|
9.  topeq(Y;b  x;c  x)
10.  topeq(Y;a  x;b  x)
\mvdash{}  topeq(Y;a  x;c  x)


By

---

Latex:
(FLemma  `topeq\_transitivity`  [-1;-2]  THEN  Auto)

---

Home Index