---

Step * of Lemma simple-glueing

∀[X:Type]. ∀[dX:metric(X)]. ∀[A,B:X ⟶ ℙ].
  ((∀x1,x2:X.  (x1 ≡ x2 ⇒ A[x1] ⇒ A[x2]))
  ⇒ (∀x1,x2:X.  (x1 ≡ x2 ⇒ B[x1] ⇒ B[x2]))
  ⇒ (∀x:X. (A[x] ∨ B[x]))
  ⇒ (∀[Y:Type]. ∀[dY:metric(Y)].
        ∀f:FUN({x:X| A[x]}  ⟶ Y). ∀g:FUN({x:X| B[x]}  ⟶ Y).
          ∃h:FUN(X ⟶ Y). ∀x:X. ((A[x] ⇒ h x ≡ f x) ∧ (B[x] ⇒ h x ≡ g x)) 
          supposing ∀x:X. ((A[x] ∧ B[x]) ⇒ f x ≡ g x)))
BY
{ (Auto THEN RenameVar `c' 7 THEN (D 0 With ⌜λx.case c x of inl(a) => f x | inr(b) => g x⌝  THENW Auto) THEN Reduce 0) }

1
.....wf..... 
1. X : Type
2. dX : metric(X)
3. A : X ⟶ ℙ
4. B : X ⟶ ℙ
5. ∀x1,x2:X.  (x1 ≡ x2 ⇒ A[x1] ⇒ A[x2])
6. ∀x1,x2:X.  (x1 ≡ x2 ⇒ B[x1] ⇒ B[x2])
7. c : ∀x:X. (A[x] ∨ B[x])
8. Y : Type
9. dY : metric(Y)
10. f : FUN({x:X| A[x]}  ⟶ Y)
11. g : FUN({x:X| B[x]}  ⟶ Y)
12. ∀x:X. ((A[x] ∧ B[x]) ⇒ f x ≡ g x)
⊢ λx.case c x of inl(a) => f x | inr(b) => g x ∈ FUN(X ⟶ Y)

2
1. [X] : Type
2. [dX] : metric(X)
3. [A] : X ⟶ ℙ
4. [B] : X ⟶ ℙ
5. ∀x1,x2:X.  (x1 ≡ x2 ⇒ A[x1] ⇒ A[x2])
6. ∀x1,x2:X.  (x1 ≡ x2 ⇒ B[x1] ⇒ B[x2])
7. c : ∀x:X. (A[x] ∨ B[x])
8. [Y] : Type
9. [dY] : metric(Y)
10. f : FUN({x:X| A[x]}  ⟶ Y)
11. g : FUN({x:X| B[x]}  ⟶ Y)
12. ∀x:X. ((A[x] ∧ B[x]) ⇒ f x ≡ g x)
⊢ ∀x:X
    ((A[x] ⇒ case c x of inl(a) => f x | inr(b) => g x ≡ f x)
    ∧ (B[x] ⇒ case c x of inl(a) => f x | inr(b) => g x ≡ g x))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[dX:metric(X)].  \mforall{}[A,B:X  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x1,x2:X.    (x1  \mequiv{}  x2  {}\mRightarrow{}  A[x1]  {}\mRightarrow{}  A[x2]))
    {}\mRightarrow{}  (\mforall{}x1,x2:X.    (x1  \mequiv{}  x2  {}\mRightarrow{}  B[x1]  {}\mRightarrow{}  B[x2]))
    {}\mRightarrow{}  (\mforall{}x:X.  (A[x]  \mvee{}  B[x]))
    {}\mRightarrow{}  (\mforall{}[Y:Type].  \mforall{}[dY:metric(Y)].
                \mforall{}f:FUN(\{x:X|  A[x]\}    {}\mrightarrow{}  Y).  \mforall{}g:FUN(\{x:X|  B[x]\}    {}\mrightarrow{}  Y).
                    \mexists{}h:FUN(X  {}\mrightarrow{}  Y).  \mforall{}x:X.  ((A[x]  {}\mRightarrow{}  h  x  \mequiv{}  f  x)  \mwedge{}  (B[x]  {}\mRightarrow{}  h  x  \mequiv{}  g  x)) 
                    supposing  \mforall{}x:X.  ((A[x]  \mwedge{}  B[x])  {}\mRightarrow{}  f  x  \mequiv{}  g  x)))


By

---

Latex:
(Auto
  THEN  RenameVar  `c'  7
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}x.case  c  x  of  inl(a)  =>  f  x  |  inr(b)  =>  g  x\mkleeneclose{}    THENW  Auto)
  THEN  Reduce  0)

---

Home Index