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. : ℤ 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