---

Step * 1 of Lemma es-le-linorder-interface


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. j : Id@i
⊢ Linorder({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )
BY
{ (InstLemma `es-le-linorder` [⌈es⌉;⌈j⌉]⋅ THENA Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. j : Id@i
5. Linorder({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
⊢ Linorder({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  j  :  Id@i
\mvdash{}  Linorder(\{e':E(X)|  loc(e')  =  j\}  ;a,b.a  \mleq{}loc  b  )


By

(InstLemma  `es-le-linorder`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index