---

Step * 1 1 of Lemma union-continuous-type-monotone


1. F : Type ⟶ Type
2. ∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])
3. A : Type
4. B : Type
5. A ⊆r B
6. x : F A@i
7. ∀[X:𝔹 ⟶ Type]. (⋃n:𝔹.F[X n] ⊆r F[⋃n:𝔹.(X n)])
8. ⋃n:𝔹.F[if n then A else B fi ] ⊆r F[⋃n:𝔹.if n then A else B fi ]
9. x = x ∈ ⋃n:𝔹.F[if n then A else B fi ]
⊢ ⋃n:𝔹.F[if n then A else B fi ] ⊆r (F B)
BY
{ Assert ⌜F[⋃n:𝔹.if n then A else B fi ] ⊆r (F B)⌝⋅ }

1
.....assertion..... 
1. F : Type ⟶ Type
2. ∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])
3. A : Type
4. B : Type
5. A ⊆r B
6. x : F A@i
7. ∀[X:𝔹 ⟶ Type]. (⋃n:𝔹.F[X n] ⊆r F[⋃n:𝔹.(X n)])
8. ⋃n:𝔹.F[if n then A else B fi ] ⊆r F[⋃n:𝔹.if n then A else B fi ]
9. x = x ∈ ⋃n:𝔹.F[if n then A else B fi ]
⊢ F[⋃n:𝔹.if n then A else B fi ] ⊆r (F B)

2
1. F : Type ⟶ Type
2. ∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])
3. A : Type
4. B : Type
5. A ⊆r B
6. x : F A@i
7. ∀[X:𝔹 ⟶ Type]. (⋃n:𝔹.F[X n] ⊆r F[⋃n:𝔹.(X n)])
8. ⋃n:𝔹.F[if n then A else B fi ] ⊆r F[⋃n:𝔹.if n then A else B fi ]
9. x = x ∈ ⋃n:𝔹.F[if n then A else B fi ]
10. F[⋃n:𝔹.if n then A else B fi ] ⊆r (F B)
⊢ ⋃n:𝔹.F[if n then A else B fi ] ⊆r (F B)

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  \mforall{}A,B:Type.    (A  \mequiv{}  B  {}\mRightarrow{}  F[A]  \mequiv{}  F[B])
3.  A  :  Type
4.  B  :  Type
5.  A  \msubseteq{}r  B
6.  x  :  F  A@i
7.  \mforall{}[X:\mBbbB{}  {}\mrightarrow{}  Type].  (\mcup{}n:\mBbbB{}.F[X  n]  \msubseteq{}r  F[\mcup{}n:\mBbbB{}.(X  n)])
8.  \mcup{}n:\mBbbB{}.F[if  n  then  A  else  B  fi  ]  \msubseteq{}r  F[\mcup{}n:\mBbbB{}.if  n  then  A  else  B  fi  ]
9.  x  =  x
\mvdash{}  \mcup{}n:\mBbbB{}.F[if  n  then  A  else  B  fi  ]  \msubseteq{}r  (F  B)


By

---

Latex:
Assert  \mkleeneopen{}F[\mcup{}n:\mBbbB{}.if  n  then  A  else  B  fi  ]  \msubseteq{}r  (F  B)\mkleeneclose{}\mcdot{}

---

Home Index