---

Step * 2 1 of Lemma list-max-map


1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. L : A List
6. 0 < ||L||
7. list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × T)
8. i : ℤ
9. z1 : T
10. <i, z1> = list-max(x.f[x];map(g;L)) ∈ (i:ℤ × T)
⊢ z1 ∈ {x:T| f[x] = i ∈ ℤ} 
BY
{ ((Assert list-max(x.f[x];map(g;L)) = <i, z1> ∈ (i:ℤ × T) BY Eq) THEN FLemma `list-max-property2` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  g  :  A  {}\mrightarrow{}  T
4.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
5.  L  :  A  List
6.  0  <  ||L||
7.  list-max(x.f[x];map(g;L))  =  ((\mlambda{}p.<fst(p),  g  (snd(p))>)  list-max(x.f[g  x];L))
8.  i  :  \mBbbZ{}
9.  z1  :  T
10.  <i,  z1>  =  list-max(x.f[x];map(g;L))
\mvdash{}  z1  \mmember{}  \{x:T|  f[x]  =  i\} 


By

---

Latex:
((Assert  list-max(x.f[x];map(g;L))  =  <i,  z1>  BY  Eq)  THEN  FLemma  `list-max-property2`  [-1]  THEN  Auto)

---

Home Index