---

Step * of Lemma i-approx-containing2

∀I:Interval. ∀a,b:ℝ.  (((a ∈ I) ∧ (b ∈ I)) ⇒ (∃n:ℕ+. ((a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n)))))
BY
{ (Auto THEN (InstLemma `compact-subinterval` [⌜I⌝;⌜[rmin(a;b), rmax(a;b)]⌝]⋅ THENA EAuto 3)) }

1
1. I : Interval@i
2. a : ℝ@i
3. b : ℝ@i
4. a ∈ I@i
5. b ∈ I@i
6. ∃n:{n:ℕ+| icompact(i-approx(I;n))} . [rmin(a;b), rmax(a;b)] ⊆ i-approx(I;n) 
⊢ ∃n:ℕ+. ((a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n)))

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}a,b:\mBbbR{}.    (((a  \mmember{}  I)  \mwedge{}  (b  \mmember{}  I))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}\msupplus{}.  ((a  \mmember{}  i-approx(I;n))  \mwedge{}  (b  \mmember{}  i-approx(I;n)))))


By

---

Latex:
(Auto  THEN  (InstLemma  `compact-subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}[rmin(a;b),  rmax(a;b)]\mkleeneclose{}]\mcdot{}  THENA  EAuto  3))

---

Home Index