---

Step * of Lemma filter_map_upto2

∀t',m:ℕ.
  ∀[T:Type]
    ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
      ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) supposing (m + 1) ≤ ||filter(P;map(f;upto(t')))||
BY
{ InductionOnNat }

1
.....basecase..... 
∀m:ℕ
  ∀[T:Type]
    ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
      ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) supposing (m + 1) ≤ ||filter(P;map(f;upto(0)))||

2
.....upcase..... 
1. t' : ℤ
2. [%1] : 0 < t'
3. ∀m:ℕ
     ∀[T:Type]
       ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
         ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) 
         supposing (m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||
⊢ ∀m:ℕ
    ∀[T:Type]
      ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
        ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) supposing (m + 1) ≤ ||filter(P;map(f;upto(t')))||

---

Latex:

---

Latex:
\mforall{}t',m:\mBbbN{}.
    \mforall{}[T:Type]
        \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.
            \mexists{}t:\mBbbN{}.  ((\muparrow{}(P  (f  t)))  \mwedge{}  (||filter(P;map(f;upto(t)))||  =  m)) 
            supposing  (m  +  1)  \mleq{}  ||filter(P;map(f;upto(t')))||


By

---

Latex:
InductionOnNat

---

Home Index