---

Step * 2 1 of Lemma trivial-homeo-image


1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. f : FUN(X ⟶ Y)
6. h1 : FUN(Y ⟶ X)
7. ∀x:X. h1 (f x) ≡ x
8. ∀y:Y. f (h1 y) ≡ y
9. x : Y
⊢ ∃a:X. x ≡ f a
BY
{ (D 0 With ⌜h1 x⌝  THEN Auto THEN RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  Y  :  Type
3.  dX  :  metric(X)
4.  dY  :  metric(Y)
5.  f  :  FUN(X  {}\mrightarrow{}  Y)
6.  h1  :  FUN(Y  {}\mrightarrow{}  X)
7.  \mforall{}x:X.  h1  (f  x)  \mequiv{}  x
8.  \mforall{}y:Y.  f  (h1  y)  \mequiv{}  y
9.  x  :  Y
\mvdash{}  \mexists{}a:X.  x  \mequiv{}  f  a


By

---

Latex:
(D  0  With  \mkleeneopen{}h1  x\mkleeneclose{}    THEN  Auto  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index