---

Step * 1 of Lemma iproper-subinterval

.....assertion..... 
∀I,J:Interval.  (icompact(I) ⇒ I ⊆ J  ⇒ iproper(I) ⇒ iproper(J))
BY
{ (RepeatFor 3 (Intro)
   THEN (InstLemma `icompact-is-rccint` [⌜I⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN (GenConcl ⌜left-endpoint(I) = a ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜right-endpoint(I) = b ∈ ℝ⌝⋅ THENA Auto)
   THEN ThinVar `I') }

1
1. J : Interval
2. a : ℝ
3. b : ℝ
⊢ [a, b] ⊆ J  ⇒ iproper([a, b]) ⇒ iproper(J)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}I,J:Interval.    (icompact(I)  {}\mRightarrow{}  I  \msubseteq{}  J    {}\mRightarrow{}  iproper(I)  {}\mRightarrow{}  iproper(J))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (InstLemma  `icompact-is-rccint`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  (GenConcl  \mkleeneopen{}left-endpoint(I)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}right-endpoint(I)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `I')

---

Home Index