Step
*
1
of Lemma
positive-lower-bound_wf
1. x : {x:ℝ| r0 < x}
2. TERMOF{small-reciprocal-real-ext:o, 1:l} x ∈ ∃k:ℕ+. ((r1/r(k)) < x)
⊢ positive-lower-bound(x) ∈ {k:ℕ+| (r1/r(k)) < x}
BY
{ (Assert positive-lower-bound(x) ~ fst((TERMOF{small-reciprocal-real-ext:o, 1:l} x)) BY
(Unfold `positive-lower-bound` 0
THEN RW (AddrC [2] (TagC (mk_tag_term 3))) 0
THEN (CallByValueReduce 0 THENA Auto)
THEN Reduce 0
THEN Auto)) }
1
1. x : {x:ℝ| r0 < x}
2. TERMOF{small-reciprocal-real-ext:o, 1:l} x ∈ ∃k:ℕ+. ((r1/r(k)) < x)
3. positive-lower-bound(x) ~ fst((TERMOF{small-reciprocal-real-ext:o, 1:l} x))
⊢ positive-lower-bound(x) ∈ {k:ℕ+| (r1/r(k)) < x}
Latex:
Latex:
1. x : \{x:\mBbbR{}| r0 < x\}
2. TERMOF\{small-reciprocal-real-ext:o, 1:l\} x \mmember{} \mexists{}k:\mBbbN{}\msupplus{}. ((r1/r(k)) < x)
\mvdash{} positive-lower-bound(x) \mmember{} \{k:\mBbbN{}\msupplus{}| (r1/r(k)) < x\}
By
Latex:
(Assert positive-lower-bound(x) \msim{} fst((TERMOF\{small-reciprocal-real-ext:o, 1:l\} x)) BY
(Unfold `positive-lower-bound` 0
THEN RW (AddrC [2] (TagC (mk\_tag\_term 3))) 0
THEN (CallByValueReduce 0 THENA Auto)
THEN Reduce 0
THEN Auto))
Home
Index