---

Step * of Lemma trivial-homeo-image

No Annotations
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. ∀[h:homeomorphic(X;dX;Y;dY)].  homeo-image(X;Y;dY;h) ≡ Y
BY
{ (Auto THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. h : homeomorphic(X;dX;Y;dY)
6. x : homeo-image(X;Y;dY;h)
⊢ x ∈ Y

2
.....subterm..... T:t
1:n
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. h : homeomorphic(X;dX;Y;dY)
6. x : Y
⊢ x ∈ homeo-image(X;Y;dY;h)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:Type].  \mforall{}[dX:metric(X)].  \mforall{}[dY:metric(Y)].  \mforall{}[h:homeomorphic(X;dX;Y;dY)].
    homeo-image(X;Y;dY;h)  \mequiv{}  Y


By

---

Latex:
(Auto  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index