---

Step * of Lemma continuous-monotone-depfunction

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

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

---

Latex:

---

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


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  Auto  THEN  RepeatFor  3  ((D  0  THEN  Try  (Complete  (Auto))))  THEN  Auto)

---

Home Index