---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[P:E(X) ─→ 𝔹]. ∀[n:ℕ]. ∀[f:ℕn ─→ {e:E(X)| ↑P[e]} ].
  ∀[k:ℕn]. n ≤ ||filter(λe.P[e];≤(X)(f k))|| supposing ∀i:ℕn. f i ≤loc f k  supposing Inj(ℕn;{e:E(X)| ↑P[e]} ;f)
BY
{ Auto }

1
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))||

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[P:E(X)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].
\mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \{e:E(X)|  \muparrow{}P[e]\}  ].
    \mforall{}[k:\mBbbN{}n].  n  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(f  k))||  supposing  \mforall{}i:\mBbbN{}n.  f  i  \mleq{}loc  f  k   
    supposing  Inj(\mBbbN{}n;\{e:E(X)|  \muparrow{}P[e]\}  ;f)


By

---

Latex:
Auto

---

Home Index