---

Step * of Lemma union-continuous-type-monotone

∀[F:Type ⟶ Type]. (Monotone(T.F[T])) supposing (union-continuous{i:l}(T.F[T]) and (∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])))
BY
{ Auto }

1
.....wf..... 
1. F : Type ⟶ Type
2. ∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])
3. union-continuous{i:l}(T.F[T])
4. A : Type
5. B : Type
6. A ⊆r B
7. x : F A@i
⊢ x ∈ F B

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    (Monotone(T.F[T]))  supposing 
          (union-continuous\{i:l\}(T.F[T])  and 
          (\mforall{}A,B:Type.    (A  \mequiv{}  B  {}\mRightarrow{}  F[A]  \mequiv{}  F[B])))


By

---

Latex:
Auto

---

Home Index