---

Step * 1 of Lemma continuous-monotone-isect


1. A : Type
2. F : A ⟶ Type ⟶ Type
3. ∀a:A. ContinuousMonotone(T.F a T)
4. X : ℕ ⟶ Type
5. x : ⋂n:ℕ. ⋂a:A.  (F a (X n))
6. a : A
⊢ x ∈ F a (⋂n:ℕ. (X n))
BY
{ (SubsumeC ⌜⋂n:ℕ. (F a (X n))⌝⋅ THEN Auto THEN BackThruSomeHyp')⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(SubsumeC  \mkleeneopen{}\mcap{}n:\mBbbN{}.  (F  a  (X  n))\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  BackThruSomeHyp')\mcdot{}

---

Home Index