---

Step * of Lemma finite-max

∀[T:Type]. (finite-type(T) ⇒ T ⇒ (∀g:T ⟶ ℤ. ∃x:T. ∀y:T. ((g y) ≤ (g x))))
BY
{ Auto }

1
1. [T] : Type
2. finite-type(T)
3. T
4. g : T ⟶ ℤ
⊢ ∃x:T. ∀y:T. ((g y) ≤ (g x))

---

Latex:

---

Latex:
\mforall{}[T:Type].  (finite-type(T)  {}\mRightarrow{}  T  {}\mRightarrow{}  (\mforall{}g:T  {}\mrightarrow{}  \mBbbZ{}.  \mexists{}x:T.  \mforall{}y:T.  ((g  y)  \mleq{}  (g  x))))


By

---

Latex:
Auto

---

Home Index