---

Step * 1 of Lemma ifun_subtype_subinterval

.....set predicate..... 
1. I : {I:Interval| icompact(I)} 
2. J : {J:Interval| icompact(J)} 
3. J ⊆ I 
4. x : I ⟶ℝ
5. ifun(x;I)
⊢ ifun(x;J)
BY
{ ((Assert icompact(I) BY
          (D 1 THEN Unhide THEN Auto))
   THEN (Assert icompact(J) BY
               (D 2 THEN Unhide THEN Auto))
   THEN Assert ⌜(left-endpoint(I) ≤ left-endpoint(J)) ∧ (right-endpoint(J) ≤ right-endpoint(I))⌝⋅) }

1
.....assertion..... 
1. I : {I:Interval| icompact(I)} 
2. J : {J:Interval| icompact(J)} 
3. J ⊆ I 
4. x : I ⟶ℝ
5. ifun(x;I)
6. icompact(I)
7. icompact(J)
⊢ (left-endpoint(I) ≤ left-endpoint(J)) ∧ (right-endpoint(J) ≤ right-endpoint(I))

2
1. I : {I:Interval| icompact(I)} 
2. J : {J:Interval| icompact(J)} 
3. J ⊆ I 
4. x : I ⟶ℝ
5. ifun(x;I)
6. icompact(I)
7. icompact(J)
8. (left-endpoint(I) ≤ left-endpoint(J)) ∧ (right-endpoint(J) ≤ right-endpoint(I))
⊢ ifun(x;J)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  I  :  \{I:Interval|  icompact(I)\} 
2.  J  :  \{J:Interval|  icompact(J)\} 
3.  J  \msubseteq{}  I 
4.  x  :  I  {}\mrightarrow{}\mBbbR{}
5.  ifun(x;I)
\mvdash{}  ifun(x;J)


By

---

Latex:
((Assert  icompact(I)  BY
                (D  1  THEN  Unhide  THEN  Auto))
  THEN  (Assert  icompact(J)  BY
                          (D  2  THEN  Unhide  THEN  Auto))
  THEN  Assert  \mkleeneopen{}(left-endpoint(I)  \mleq{}  left-endpoint(J))  \mwedge{}  (right-endpoint(J)  \mleq{}  right-endpoint(I))\mkleeneclose{}\mcdot{})

---

Home Index