---

Step * 2 2 of Lemma i-finite-iff-bounded


1. I : Interval
2. a : ℝ
3. b : ℝ
4. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
5. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ i-finite(I)
BY
{ ((D 1 THEN D 1 THEN D 2)
   THEN RepUR ``i-finite`` 0
   THEN Try (Complete (Auto))
   THEN Try (DVar `x')
   THEN RepUR ``i-member`` -2) }

1
1. x1 : ℝ
2. y : Top
3. a : ℝ
4. b : ℝ
5. ∀[r:ℝ]. a≤r≤b supposing x1 ≤ r
6. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ True ∧ False

2
1. y1 : ℝ
2. y : Top
3. a : ℝ
4. b : ℝ
5. ∀[r:ℝ]. a≤r≤b supposing y1 < r
6. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ True ∧ False

3
1. y : Top
2. x1 : ℝ
3. a : ℝ
4. b : ℝ
5. ∀[r:ℝ]. a≤r≤b supposing r ≤ x1
6. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ False ∧ True

4
1. y : Top
2. y1 : ℝ
3. a : ℝ
4. b : ℝ
5. ∀[r:ℝ]. a≤r≤b supposing r < y1
6. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ False ∧ True

5
1. y : Top
2. y1 : Top
3. a : ℝ
4. b : ℝ
5. ∀[r:ℝ]. a≤r≤b supposing True
6. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ False ∧ False

---

Latex:

---

Latex:

1.  I  :  Interval
2.  a  :  \mBbbR{}
3.  b  :  \mBbbR{}
4.  \mforall{}[r:\mBbbR{}].  a\mleq{}r\mleq{}b  supposing  r  \mmember{}  I
5.  (\mneg{}((b  +  r1)  \mleq{}  b))  \mwedge{}  (\mneg{}(a  \mleq{}  (a  -  r1)))
\mvdash{}  i-finite(I)


By

---

Latex:
((D  1  THEN  D  1  THEN  D  2)
  THEN  RepUR  ``i-finite``  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  (DVar  `x')
  THEN  RepUR  ``i-member``  -2)

---

Home Index