---

Step * 1 of Lemma glues-property2


1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ia : EClass(A)@i'
6. Ib : EClass(B)@i'
7. ∀f:E(Ia) ⟶ B. ∀g:E(Ib) ⟶ E(Ia).
     (g glues Ia ──f⟶ Ib
     ⇐⇒ {Bij(E(Ib);E(Ia);g)
         ∧ (∀e:E(Ib). g e c≤ e)
         ∧ (∀e,e':E(Ib).  (g e ≤loc g e'  ⇒ e ≤loc e' ))
         ∧ (∀e:E(Ib). ((f (g e)) = Ib(e) ∈ B))})
8. f : E(Ia) ⟶ B@i
9. g : E(Ib) ⟶ E@i
10. g glues Ia ──f⟶ Ib@i
⊢ {Bij(E(Ib);E(Ia);g)
∧ (∀e:E(Ib). g e c≤ e)
∧ (∀e,e':E(Ib).  (g e ≤loc g e'  ⇒ e ≤loc e' ))
∧ (∀e:E(Ib). ((f (g e)) = Ib(e) ∈ B))}
BY
{ ((FLemma `glues-property` [-1] THENA Auto) THEN (InstHyp [⌜f⌝;⌜g⌝] 7⋅ THENA Auto) THEN ThinTrivial THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [A]  :  Type
4.  [B]  :  Type
5.  Ia  :  EClass(A)@i'
6.  Ib  :  EClass(B)@i'
7.  \mforall{}f:E(Ia)  {}\mrightarrow{}  B.  \mforall{}g:E(Ib)  {}\mrightarrow{}  E(Ia).
          (g  glues  Ia  {}{}f{}\mrightarrow{}  Ib
          \mLeftarrow{}{}\mRightarrow{}  \{Bij(E(Ib);E(Ia);g)
                  \mwedge{}  (\mforall{}e:E(Ib).  g  e  c\mleq{}  e)
                  \mwedge{}  (\mforall{}e,e':E(Ib).    (g  e  \mleq{}loc  g  e'    {}\mRightarrow{}  e  \mleq{}loc  e'  ))
                  \mwedge{}  (\mforall{}e:E(Ib).  ((f  (g  e))  =  Ib(e)))\})
8.  f  :  E(Ia)  {}\mrightarrow{}  B@i
9.  g  :  E(Ib)  {}\mrightarrow{}  E@i
10.  g  glues  Ia  {}{}f{}\mrightarrow{}  Ib@i
\mvdash{}  \{Bij(E(Ib);E(Ia);g)
\mwedge{}  (\mforall{}e:E(Ib).  g  e  c\mleq{}  e)
\mwedge{}  (\mforall{}e,e':E(Ib).    (g  e  \mleq{}loc  g  e'    {}\mRightarrow{}  e  \mleq{}loc  e'  ))
\mwedge{}  (\mforall{}e:E(Ib).  ((f  (g  e))  =  Ib(e)))\}


By

---

Latex:
((FLemma  `glues-property`  [-1]  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index