Proof of Nuprl Lemma : homeomorphic

Step * of Lemma homeomorphic_weakening

∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)].  (X ≡ Y ⇒ (dX = dY ∈ metric(X)) ⇒ homeomorphic(X;dX;Y;dY))
BY
{ ((Auto
    THEN (Assert λx.x ∈ FUN(X ⟶ Y) BY
                (MemTypeCD
                 THEN Auto
                 THEN D 0
                 THEN Reduce 0
                 THEN Auto
                 THEN RepUR ``so_apply`` 0
                 THEN RWO "6<" 0
                 THEN Auto))
    THEN (Assert λx.x ∈ FUN(Y ⟶ X) BY
                (MemTypeCD
                 THEN Auto
                 THEN D 0
                 THEN Reduce 0
                 THEN Auto
                 THEN RepUR ``so_apply`` 0
                 THEN RWO "6" 0
                 THEN Auto)))
   THEN RepeatFor 2 ((D 0 With ⌜λx.x⌝  THENA Auto))
   ) }

1
1. [X] : Type
2. [Y] : Type
3. [dX] : metric(X)
4. [dY] : metric(Y)
5. X ≡ Y
6. dX = dY ∈ metric(X)
7. λx.x ∈ FUN(X ⟶ Y)
8. λx.x ∈ FUN(Y ⟶ X)
⊢ (∀x:X. (λx.x) ((λx.x) x) ≡ x) ∧ (∀y:Y. (λx.x) ((λx.x) y) ≡ y)

Latex:

Latex:
\mforall{}[X,Y:Type]. \mforall{}[dX:metric(X)]. \mforall{}[dY:metric(Y)]. (X \mequiv{} Y {}\mRightarrow{} (dX = dY) {}\mRightarrow{} homeomorphic(X;dX;Y;dY)) By Latex: ((Auto THEN (Assert \mlambda{}x.x \mmember{} FUN(X {}\mrightarrow{} Y) BY (MemTypeCD THEN Auto THEN D 0 THEN Reduce 0 THEN Auto THEN RepUR ``so\_apply`` 0 THEN RWO "6<" 0 THEN Auto)) THEN (Assert \mlambda{}x.x \mmember{} FUN(Y {}\mrightarrow{} X) BY (MemTypeCD THEN Auto THEN D 0 THEN Reduce 0 THEN Auto THEN RepUR ``so\_apply`` 0 THEN RWO "6" 0 THEN Auto))) THEN RepeatFor 2 ((D 0 With \mkleeneopen{}\mlambda{}x.x\mkleeneclose{} THENA Auto)) ) Home Index