---

Step * of Lemma i-member-diff-bound

∀I:Interval. (icompact(I) ⇒ (∀x,y:{x:ℝ| x ∈ I} .  (|x - y| ≤ |I|)))
BY
{ (Auto
   THEN DSetVars 
   THEN Unhide
   THEN Auto
   THEN ∀h:hyp. ((FLemma `i-member-compact` [h] THENA Auto) THEN D -1 THEN RepeatFor 2 (MoveToConcl (-1))) 
   THEN Unfold `i-length` 0
   THEN GenConclTerms Auto [⌜left-endpoint(I)⌝;⌜right-endpoint(I)⌝]⋅
   THEN All Thin
   THEN RenameVar `a' (-2)
   THEN RenameVar `b' (-1)
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. a : ℝ
4. b : ℝ
5. a ≤ x
6. x ≤ b
7. a ≤ y
8. y ≤ b
⊢ |x - y| ≤ (b - a)

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (|x  -  y|  \mleq{}  |I|)))


By

---

Latex:
(Auto
  THEN  DSetVars 
  THEN  Unhide
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((FLemma  `i-member-compact`  [h]  THENA  Auto)
                              THEN  D  -1
                              THEN  RepeatFor  2  (MoveToConcl  (-1))) 
  THEN  Unfold  `i-length`  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}left-endpoint(I)\mkleeneclose{};\mkleeneopen{}right-endpoint(I)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  RenameVar  `a'  (-2)
  THEN  RenameVar  `b'  (-1)
  THEN  Auto)

---

Home Index