---

Step * of Lemma imax-class-lb

∀[Info,T:Type]. ∀[f:T ⟶ ℤ]. ∀[es:EO+(Info)]. ∀[lb:ℤ]. ∀[X:EClass(T)]. ∀[e:E(X)]. ∀[n:ℤ].
  uiff((maximum f[v] ≥ lb with v from X)(e) ≤ n;(∀[e':E(X)]. f[X(e')] ≤ n supposing e' ≤loc e ) ∧ (lb ≤ n))
BY
{ ((UnivCD THENA Auto) THEN (RWW "imax-class-val imax-list-lb" 0 THENA (Auto THEN RWO "is-imax-class" 0 THEN Auto))) }

1
1. Info : Type
2. T : Type
3. f : T ⟶ ℤ
4. es : EO+(Info)
5. lb : ℤ
6. X : EClass(T)
7. e : E(X)
8. n : ℤ
⊢ uiff((∀b∈[lb / map(λv.f[v];X(≤(X)(e)))].b ≤ n);(∀[e':E(X)]. f[X(e')] ≤ n supposing e' ≤loc e ) ∧ (lb ≤ n))

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[es:EO+(Info)].  \mforall{}[lb:\mBbbZ{}].  \mforall{}[X:EClass(T)].  \mforall{}[e:E(X)].  \mforall{}[n:\mBbbZ{}].
    uiff((maximum  f[v]  \mgeq{}  lb  with  v  from  X)(e)  \mleq{}  n;(\mforall{}[e':E(X)].  f[X(e')]  \mleq{}  n  supposing  e'  \mleq{}loc  e  )
    \mwedge{}  (lb  \mleq{}  n))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWW  "imax-class-val  imax-list-lb"  0  THENA  (Auto  THEN  RWO  "is-imax-class"  0  THEN  Auto))
  )

---

Home Index