Step
*
of Lemma
imax-list-subset
∀[L,L':ℤ List]. (imax-list(L) ≤ imax-list(L')) supposing (l_subset(ℤ;L;L') and 0 < ||L||)
BY
{ ((Auto THEN (FLemma `l_subset_pos_length` [3;4] THEN Auto)⋅) THEN BLemma `imax-list-lb` THEN Auto) }
1
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. l_subset(ℤ;L;L')
5. 0 < ||L'||
⊢ (∀b∈L.b ≤ imax-list(L'))
Latex:
Latex:
\mforall{}[L,L':\mBbbZ{} List]. (imax-list(L) \mleq{} imax-list(L')) supposing (l\_subset(\mBbbZ{};L;L') and 0 < ||L||)
By
Latex:
((Auto THEN (FLemma `l\_subset\_pos\_length` [3;4] THEN Auto)\mcdot{}) THEN BLemma `imax-list-lb` THEN Auto)
Home
Index