---

Step * of Lemma continuous'-monotone-bunion

∀[F,G:Type ⟶ Type].
  (continuous'-monotone{i:l}(T.F[T] ⋃ G[T])) supposing 
     (continuous'-monotone{i:l}(T.G[T]) and 
     continuous'-monotone{i:l}(T.F[T]))
BY
{ (RepUR ``so_apply continuous\'-monotone`` 0 THEN Auto THEN All UnfoldTopAb THEN Auto THEN D 0 THEN Auto) }

1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. ∀[A,B:Type].  (F A) ⊆r (F B) supposing A ⊆r B
4. ∀[X:type-incr-chain{i:l}()]. ((F ⋃n:ℕ.(X n)) ⊆r ⋃n:ℕ.(F (X n)))
5. ∀[A,B:Type].  (G A) ⊆r (G B) supposing A ⊆r B
6. ∀[X:type-incr-chain{i:l}()]. ((G ⋃n:ℕ.(X n)) ⊆r ⋃n:ℕ.(G (X n)))
7. ∀[A,B:Type].  ((F A) ⋃ (G A)) ⊆r ((F B) ⋃ (G B)) supposing A ⊆r B
8. X : type-incr-chain{i:l}()
9. x : (F ⋃n:ℕ.(X n)) ⋃ (G ⋃n:ℕ.(X n))@i
⊢ x ∈ ⋃n:ℕ.((F (X n)) ⋃ (G (X n)))

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (continuous'-monotone\{i:l\}(T.F[T]  \mcup{}  G[T]))  supposing 
          (continuous'-monotone\{i:l\}(T.G[T])  and 
          continuous'-monotone\{i:l\}(T.F[T]))


By

---

Latex:
(RepUR  ``so\_apply  continuous\mbackslash{}'-monotone``  0
  THEN  Auto
  THEN  All  UnfoldTopAb
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index