---

Step * of Lemma maximal-in-list

∀[A:Type]. ∀f:A ⟶ ℤ. ∀L:A List.  (∃a∈L. (∀x∈L.(f x) ≤ (f a))) supposing 0 < ||L||
BY
{ (InstLemma `list-max-property` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }

1
1. [A] : Type
2. f : A ⟶ ℤ
3. L : A List
4. 0 < ||L||
5. let n,x = list-max(x.f[x];L) 
   in (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n)
⊢ (∃a∈L. (∀x∈L.(f x) ≤ (f a)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}f:A  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:A  List.    (\mexists{}a\mmember{}L.  (\mforall{}x\mmember{}L.(f  x)  \mleq{}  (f  a)))  supposing  0  <  ||L||


By

---

Latex:
(InstLemma  `list-max-property`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto)

---

Home Index