---

Step * of Lemma strong-continuity2_biject_retract

∀[T,S,U:Type].
  ∀r:ℕ ⟶ U
    ((U ⊆r ℕ)
    ⇒ (∀x:U. ((r x) = x ∈ U))
    ⇒ (∀g:S ⟶ U
          (Bij(S;U;g)
          ⇒ (∀F:(ℕ ⟶ T) ⟶ S
                (strong-continuity2(T;g o F)
                ⇒ (∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
                     ∀f:ℕ ⟶ T
                       ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?)))
                       ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))))))))
BY
{ (Auto THEN D -1 THEN Reduce -1 THEN FLemma `biject-inverse` [-4] THEN Auto THEN D -1 THEN RenameVar `h' (-2)) }

1
1. [T] : Type
2. [S] : Type
3. [U] : Type
4. r : ℕ ⟶ U@i
5. U ⊆r ℕ
6. ∀x:U. ((r x) = x ∈ U)
7. g : S ⟶ U@i
8. Bij(S;U;g)
9. F : (ℕ ⟶ T) ⟶ S@i
10. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)@i
11. ∀f:ℕ ⟶ T
      ((∃n:ℕ. ((M n f) = (inl (g (F f))) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (g (F f))) ∈ (ℕ?) supposing ↑isl(M n f)))
12. h : U ⟶ S
13. (∀b:U. ((g (h b)) = b ∈ U)) ∧ (∀a:S. ((h (g a)) = a ∈ S))
⊢ ∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
   ∀f:ℕ ⟶ T. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))

---

Latex:

---

Latex:
\mforall{}[T,S,U:Type].
    \mforall{}r:\mBbbN{}  {}\mrightarrow{}  U
        ((U  \msubseteq{}r  \mBbbN{})
        {}\mRightarrow{}  (\mforall{}x:U.  ((r  x)  =  x))
        {}\mRightarrow{}  (\mforall{}g:S  {}\mrightarrow{}  U
                    (Bij(S;U;g)
                    {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  S
                                (strong-continuity2(T;g  o  F)
                                {}\mRightarrow{}  (\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (S?)
                                          \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
                                              ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))
                                              \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f)))))))))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Reduce  -1
  THEN  FLemma  `biject-inverse`  [-4]
  THEN  Auto
  THEN  D  -1
  THEN  RenameVar  `h'  (-2))

---

Home Index