---

Step * of Lemma filter-for-max

∀[A:Type]. ∀[l:A List]. ∀[m:ℤ]. ∀[g:A ⟶ ℤ].
  (||filter(λe.(g[e] =z m);l)|| ≥ 1 ) supposing ((imax-list(map(λe.g[e];l)) = m ∈ ℤ) and 0 < ||l||)
BY
{ (RepUR ``so_apply`` 0 THEN Auto THEN Try ((RWO "map_length" 0 THEN Auto))) }

1
1. A : Type
2. l : A List
3. m : ℤ
4. g : A ⟶ ℤ
5. 0 < ||l||
6. imax-list(map(λe.(g e);l)) = m ∈ ℤ
⊢ ||filter(λe.(g e =z m);l)|| ≥ 1 

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].  \mforall{}[m:\mBbbZ{}].  \mforall{}[g:A  {}\mrightarrow{}  \mBbbZ{}].
    (||filter(\mlambda{}e.(g[e]  =\msubz{}  m);l)||  \mgeq{}  1  )  supposing  ((imax-list(map(\mlambda{}e.g[e];l))  =  m)  and  0  <  ||l||)


By

---

Latex:
(RepUR  ``so\_apply``  0  THEN  Auto  THEN  Try  ((RWO  "map\_length"  0  THEN  Auto)))

---

Home Index