---

Step * of Lemma continuous-monotone-isect

∀[A:Type]. ∀[F:A ⟶ Type ⟶ Type].  ContinuousMonotone(T.⋂a:A. F[a;T]) supposing ∀a:A. ContinuousMonotone(T.F[a;T])
BY
{ (Unfold `so_apply` 0 THEN Auto THEN Repeat ((D 0 THEN Auto))) }

1
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))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[F:A  {}\mrightarrow{}  Type  {}\mrightarrow{}  Type].
    ContinuousMonotone(T.\mcap{}a:A.  F[a;T])  supposing  \mforall{}a:A.  ContinuousMonotone(T.F[a;T])


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  Auto  THEN  Repeat  ((D  0  THEN  Auto)))

---

Home Index