---

Step * of Lemma bag-max_wf

No Annotations
∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)].  bag-max(f;bs) ∈ ℤ supposing 0 < #(bs)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[bs:bag(A)].    bag-max(f;bs)  \mmember{}  \mBbbZ{}  supposing  0  <  \#(bs)


By

---

Latex:
ProveWfLemma

---

Home Index