---

Step * of Lemma continuous-monotone-set

∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (ContinuousMonotone(T.{x:F[T]| P[x]} )) supposing ((∀T:Type. (F[T] ⊆r A)) and ContinuousMonotone(T.F[T]))
BY
{ (Unfold `so_apply` 0 THEN Auto THEN D 0 THEN D (-2) THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
.....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} 

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[F:Type  {}\mrightarrow{}  Type].
    (ContinuousMonotone(T.\{x:F[T]|  P[x]\}  ))  supposing  ((\mforall{}T:Type.  (F[T]  \msubseteq{}r  A))  and  ContinuousMonotone(T\000C.F[T]))


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  Auto  THEN  D  0  THEN  D  (-2)  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index