---

Step * 1 of Lemma continuous-monotone-depfunction

.....subterm..... T:t
1:n
1. A : Type
2. F : Type ⟶ A ⟶ Type
3. ∀a:A. ContinuousMonotone(T.F T a)
4. X : ℕ ⟶ Type
5. x : ⋂n:ℕ. (a:A ⟶ (F (X n) a))@i
⊢ x ∈ a:A ⟶ (F (⋂n:ℕ. (X n)) a)
BY
{ (SubsumeC ⌜a:A ⟶ (⋂n:ℕ. (F (X n) a))⌝⋅ THEN Auto THEN ExtWith [`a'] [⌜a:A ⟶ (F (X 0) a)⌝]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  F  :  Type  {}\mrightarrow{}  A  {}\mrightarrow{}  Type
3.  \mforall{}a:A.  ContinuousMonotone(T.F  T  a)
4.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
5.  x  :  \mcap{}n:\mBbbN{}.  (a:A  {}\mrightarrow{}  (F  (X  n)  a))@i
\mvdash{}  x  \mmember{}  a:A  {}\mrightarrow{}  (F  (\mcap{}n:\mBbbN{}.  (X  n))  a)


By

---

Latex:
(SubsumeC  \mkleeneopen{}a:A  {}\mrightarrow{}  (\mcap{}n:\mBbbN{}.  (F  (X  n)  a))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ExtWith  [`a']  [\mkleeneopen{}a:A  {}\mrightarrow{}  (F  (X  0)  a)\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index