Step
*
2
of Lemma
partition-point-member
1. I : Interval
2. icompact(I)
3. p : ℝ List
4. frs-non-dec(p)
5. i : ℕ||p||
6. (left-endpoint(I) ≤ p[0]) ∧ (last(p) ≤ right-endpoint(I))
⊢ p[i] ≤ right-endpoint(I)
BY
{ ((With ⌜i⌝ (D (-3))⋅ THENM InstHyp [⌜||p|| - 1⌝] (-1)⋅)
THEN Auto
THEN Fold `last` (-1)
THEN Try ((RelRST THEN Auto))) }
Latex:
Latex:
1. I : Interval
2. icompact(I)
3. p : \mBbbR{} List
4. frs-non-dec(p)
5. i : \mBbbN{}||p||
6. (left-endpoint(I) \mleq{} p[0]) \mwedge{} (last(p) \mleq{} right-endpoint(I))
\mvdash{} p[i] \mleq{} right-endpoint(I)
By
Latex:
((With \mkleeneopen{}i\mkleeneclose{} (D (-3))\mcdot{} THENM InstHyp [\mkleeneopen{}||p|| - 1\mkleeneclose{}] (-1)\mcdot{})
THEN Auto
THEN Fold `last` (-1)
THEN Try ((RelRST THEN Auto)))
Home
Index