Step
*
of Lemma
reals-close-or-rneq
No Annotations
∀K:ℕ+
(∃g:ℝ ⟶ ℝ ⟶ ℕ3 [(∀x,y:ℝ.
((((g x y) = 1 ∈ ℤ)
⇒ ((r1/r(K)) < (y - x)))
∧ (((g x y) = 2 ∈ ℤ)
⇒ ((r1/r(K)) < (x - y)))
∧ (((g x y) = 0 ∈ ℤ)
⇒ (|x - y| < (r(2)/r(K))))))])
BY
{ (Auto THEN (InstLemma `int-rdiv-rless-witness2` [⌜K⌝]⋅ THENA Auto)) }
1
1. K : ℕ+
2. 3 * K ∈ (r1)/K < (r(2))/K
⊢ ∃g:ℝ ⟶ ℝ ⟶ ℕ3 [(∀x,y:ℝ.
((((g x y) = 1 ∈ ℤ)
⇒ ((r1/r(K)) < (y - x)))
∧ (((g x y) = 2 ∈ ℤ)
⇒ ((r1/r(K)) < (x - y)))
∧ (((g x y) = 0 ∈ ℤ)
⇒ (|x - y| < (r(2)/r(K))))))]
Latex:
Latex:
No Annotations
\mforall{}K:\mBbbN{}\msupplus{}
(\mexists{}g:\mBbbR{} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbN{}3 [(\mforall{}x,y:\mBbbR{}.
((((g x y) = 1) {}\mRightarrow{} ((r1/r(K)) < (y - x)))
\mwedge{} (((g x y) = 2) {}\mRightarrow{} ((r1/r(K)) < (x - y)))
\mwedge{} (((g x y) = 0) {}\mRightarrow{} (|x - y| < (r(2)/r(K))))))])
By
Latex:
(Auto THEN (InstLemma `int-rdiv-rless-witness2` [\mkleeneopen{}K\mkleeneclose{}]\mcdot{} THENA Auto))
Home
Index