---

Step * of Lemma ifun_subtype_subinterval

∀[I,J:{J:Interval| icompact(J)} ].  {f:I ⟶ℝ| ifun(f;I)}  ⊆r {f:J ⟶ℝ| ifun(f;J)}  supposing J ⊆ I 
BY
{ (Auto THEN (D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto) }

1
.....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)

---

Latex:

---

Latex:
\mforall{}[I,J:\{J:Interval|  icompact(J)\}  ].    \{f:I  {}\mrightarrow{}\mBbbR{}|  ifun(f;I)\}    \msubseteq{}r  \{f:J  {}\mrightarrow{}\mBbbR{}|  ifun(f;J)\}    supposing  J  \msubseteq{}  I 


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index