---

Step * 1 of Lemma filter-interface-predecessors-lower-bound3


1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. n : ℕ+@i
7. f : ℕn ─→ {e:E(X)| ↑P[e]} @i
8. Inj(ℕn;{e:E(X)| ↑P[e]} ;f)
9. ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)
⊢ ∃e:{e:E(X)| ↑P[e]} . (n ≤ ||filter(λe.P[e];≤(X)(e))||)
BY
{ ((InstLemma `last-event-of-set` [⌈es⌉;⌈n⌉;⌈f⌉]⋅ THENM D -1) THENA Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. n : ℕ+@i
7. f : ℕn ─→ {e:E(X)| ↑P[e]} @i
8. Inj(ℕn;{e:E(X)| ↑P[e]} ;f)
9. ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)
10. k : ℕn
11. ∀i:ℕn. f i ≤loc f k 
⊢ ∃e:{e:E(X)| ↑P[e]} . (n ≤ ||filter(λe.P[e];≤(X)(e))||)

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [T]  :  Type
4.  X  :  EClass(T)@i'
5.  P  :  E(X)  {}\mrightarrow{}  \mBbbB{}@i
6.  n  :  \mBbbN{}\msupplus{}@i
7.  f  :  \mBbbN{}n  {}\mrightarrow{}  \{e:E(X)|  \muparrow{}P[e]\}  @i
8.  Inj(\mBbbN{}n;\{e:E(X)|  \muparrow{}P[e]\}  ;f)
9.  \mforall{}i,j:\mBbbN{}n.    (loc(f  i)  =  loc(f  j))
\mvdash{}  \mexists{}e:\{e:E(X)|  \muparrow{}P[e]\}  .  (n  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||)


By

---

Latex:
((InstLemma  `last-event-of-set`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THENA  Auto)

---

Home Index