---

Step * 1 of Lemma continuous-monotone-set

.....subterm..... T:t
1:n
1. A : Type
2. P : A ⟶ ℙ
3. F : Type ⟶ Type
4. Monotone(T.F T)
5. Continuous(T.F T)
6. ∀T:Type. ((F T) ⊆r A)
7. X : ℕ ⟶ Type
8. x : ⋂n:ℕ. {x:F (X n)| P x} @i
⊢ x ∈ {x:F (⋂n:ℕ. (X n))| P x} 
BY
{ ((Assert x ∈ {x:F (X 0)| P x}  BY
          (With ⌜0⌝ (D (-1))⋅ THEN Auto))
   THEN (MemTypeHD (-1) THENA Auto)
   THEN (MemTypeCD THENA Auto))⋅ }

1
1. A : Type
2. P : A ⟶ ℙ
3. F : Type ⟶ Type
4. Monotone(T.F T)
5. Continuous(T.F T)
6. ∀T:Type. ((F T) ⊆r A)
7. X : ℕ ⟶ Type
8. x : ⋂n:ℕ. {x:F (X n)| P x} @i
9. x = x ∈ (F (X 0))
10. P x
⊢ x ∈ F (⋂n:ℕ. (X n))

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbP{}
3.  F  :  Type  {}\mrightarrow{}  Type
4.  Monotone(T.F  T)
5.  Continuous(T.F  T)
6.  \mforall{}T:Type.  ((F  T)  \msubseteq{}r  A)
7.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
8.  x  :  \mcap{}n:\mBbbN{}.  \{x:F  (X  n)|  P  x\}  @i
\mvdash{}  x  \mmember{}  \{x:F  (\mcap{}n:\mBbbN{}.  (X  n))|  P  x\} 


By

---

Latex:
((Assert  x  \mmember{}  \{x:F  (X  0)|  P  x\}    BY
                (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto))
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  (MemTypeCD  THENA  Auto))\mcdot{}

---

Home Index