---

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

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀P:E(X) ⟶ 𝔹. ∀n:ℕ. ∀e:E.
        ∃f:ℕn ⟶ {e':E(X)| (↑P[e']) ∧ e' ≤loc e } . ∀i,j:ℕn.  (f i <loc f j) supposing i < j 
        supposing n ≤ ||filter(λe.P[e];≤(X)(e))||
BY
{ 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. e : E@i
8. n ≤ ||filter(λe.P[e];≤(X)(e))||
⊢ ∃f:ℕn ⟶ {e':E(X)| (↑P[e']) ∧ e' ≤loc e } . ∀i,j:ℕn.  (f i <loc f j) supposing i < j

---

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{}e:E.
                \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \{e':E(X)|  (\muparrow{}P[e'])  \mwedge{}  e'  \mleq{}loc  e  \}  .  \mforall{}i,j:\mBbbN{}n.    (f  i  <loc  f  j)  supposing  i  <  j 
                supposing  n  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||


By

---

Latex:
Auto

---

Home Index