Step
*
1
1
of Lemma
ifun-continuous
1. I : Interval
2. icompact(I)
3. f : {f:I ⟶ℝ| ifun(f;I)}
4. I ~ [left-endpoint(I), right-endpoint(I)]
5. left-endpoint(I) ≤ right-endpoint(I)
⊢ real-cont(λ2x.f[x];left-endpoint(I);right-endpoint(I))
BY
{ (BLemma `real-fun-iff-continuous` THEN Auto THEN (Assert ifun(f;I) BY (DVar `f' THEN Unhide THEN Auto))) }
1
1. I : Interval
2. icompact(I)
3. f : {f:I ⟶ℝ| ifun(f;I)}
4. I ~ [left-endpoint(I), right-endpoint(I)]
5. left-endpoint(I) ≤ right-endpoint(I)
6. ifun(f;I)
⊢ real-fun(λ2x.f[x];left-endpoint(I);right-endpoint(I))
Latex:
Latex:
1. I : Interval
2. icompact(I)
3. f : \{f:I {}\mrightarrow{}\mBbbR{}| ifun(f;I)\}
4. I \msim{} [left-endpoint(I), right-endpoint(I)]
5. left-endpoint(I) \mleq{} right-endpoint(I)
\mvdash{} real-cont(\mlambda{}\msubtwo{}x.f[x];left-endpoint(I);right-endpoint(I))
By
Latex:
(BLemma `real-fun-iff-continuous`
THEN Auto
THEN (Assert ifun(f;I) BY
(DVar `f' THEN Unhide THEN Auto)))
Home
Index