---

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


1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. P : E(X) ─→ 𝔹
6. n : ℕ
7. f : ℕn ─→ {e:E(X)| ↑P[e]} 
8. Inj(ℕn;{e:E(X)| ↑P[e]} ;f)
9. k : ℕn
10. ∀i:ℕn. f i ≤loc f k 
⊢ n ≤ ||filter(λe.P[e];≤(X)(f k))||
BY
{ Assert ⌈∀i:ℕn. (f i ∈ filter(λe.P[e];≤(X)(f k)))⌉⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}i:\mBbbN{}n.  (f  i  \mmember{}  filter(\mlambda{}e.P[e];\mleq{}(X)(f  k)))\mkleeneclose{}\mcdot{}

---

Home Index