Step
*
of Lemma
real-continuity
No Annotations
∀a,b:ℝ. ∀f:[a, b] ⟶ℝ. real-cont(f;a;b) supposing real-fun(f;a;b) supposing a ≤ b
BY
{ (Auto
THEN (Assert mcomplete({x:ℝ| x ∈ [a, b]} with rmetric()) BY
Auto)
THEN (Assert m-TB({x:ℝ| x ∈ [a, b]} ;rmetric()) BY
Auto)
THEN (Assert mcompact({x:ℝ| x ∈ [a, b]} ;rmetric()) BY
(D 0 THEN Auto))
THEN RenameVar `cmpct' (-1)
THEN (InstLemma `compact-metric-to-real-continuity` [⌜{x:ℝ| x ∈ [a, b]} ⌝;⌜rmetric()⌝;⌜cmpct⌝;⌜f⌝]⋅
THENA (Auto THEN MemTypeCD THEN Auto THEN Unfold `is-mfun` 0 THEN RWO "rmetric-meq" 0 THEN Auto)
)
THEN NthHypSq (-1)
THEN RepUR ``m-unif-cont real-cont mdist rmetric`` 0
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}a,b:\mBbbR{}. \mforall{}f:[a, b] {}\mrightarrow{}\mBbbR{}. real-cont(f;a;b) supposing real-fun(f;a;b) supposing a \mleq{} b
By
Latex:
(Auto
THEN (Assert mcomplete(\{x:\mBbbR{}| x \mmember{} [a, b]\} with rmetric()) BY
Auto)
THEN (Assert m-TB(\{x:\mBbbR{}| x \mmember{} [a, b]\} ;rmetric()) BY
Auto)
THEN (Assert mcompact(\{x:\mBbbR{}| x \mmember{} [a, b]\} ;rmetric()) BY
(D 0 THEN Auto))
THEN RenameVar `cmpct' (-1)
THEN (InstLemma `compact-metric-to-real-continuity` [\mkleeneopen{}\{x:\mBbbR{}| x \mmember{} [a, b]\} \mkleeneclose{};\mkleeneopen{}rmetric()\mkleeneclose{};\mkleeneopen{}cmpct\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
THENA (Auto
THEN MemTypeCD
THEN Auto
THEN Unfold `is-mfun` 0
THEN RWO "rmetric-meq" 0
THEN Auto)
)
THEN NthHypSq (-1)
THEN RepUR ``m-unif-cont real-cont mdist rmetric`` 0
THEN Auto)
Home
Index