---

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

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀P:E(X) ─→ 𝔹. ∀n:ℕ+. ∀f:ℕn ─→ {e:E(X)| ↑P[e]} .
        (∃e:{e:E(X)| ↑P[e]} . (n ≤ ||filter(λe.P[e];≤(X)(e))||)) supposing 
           ((∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)) and 
           Inj(ℕn;{e:E(X)| ↑P[e]} ;f))
BY
{ (Auto THEN Try ((DoSubsume THEN 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)
⊢ ∃e:{e:E(X)| ↑P[e]} . (n ≤ ||filter(λe.P[e];≤(X)(e))||)

---

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


By

---

Latex:
(Auto  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index