---

Step * of Lemma first-at-filter-interface-predecessors

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[P:E(X) ⟶ 𝔹]. ∀[n:ℕ+]. ∀[e:E]. ∀[i:Id].
  ↑e ∈b X supposing e is first@ i s.t.  q.||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ
BY
{ (Auto THEN FLemma `first-at-filter-interface-predecessors1` [-1] THEN Auto) }

---

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{}\msupplus{}].  \mforall{}[e:E].  \mforall{}[i:Id].
    \muparrow{}e  \mmember{}\msubb{}  X  supposing  e  is  first@  i  s.t.    q.||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n


By

---

Latex:
(Auto  THEN  FLemma  `first-at-filter-interface-predecessors1`  [-1]  THEN  Auto)

---

Home Index