Step
*
of Lemma
infn_functionality
No Annotations
∀n:ℕ. ∀I:{I:Interval| icompact(I)} . ∀f,g:I^n ⟶ ℝ.
((∀x,y:I^n. (req-vec(n;x;y)
⇒ ((f x) = (f y))))
⇒ (∀x:I^n. ((f x) = (g x)))
⇒ ((infn(n;I) f) = (infn(n;I) g)))
BY
{ (Assert ∀n1:ℕ
(∀I:{I:Interval| icompact(I)} . ∀f,g:I^n1 ⟶ ℝ.
((∀x,y:I^n1. (req-vec(n1;x;y)
⇒ ((f x) = (f y))))
⇒ (∀x:I^n1. ((f x) = (g x)))
⇒ ((infn(n1;I) f) = (infn(n1;I) g))) ∈ ℙ) BY
((D 0 THENA Auto)
THEN RepeatFor 5 ((MemCD THENL [Auto; Id]))
THEN (Assert ∀x,y:I^n1. (req-vec(n1;x;y)
⇒ ((g x) = (g y))) BY
(RWO "-1<" 0 THEN Auto))
THEN RepeatFor 2 (MemCD)
THEN Auto)) }
1
1. ∀n1:ℕ
(∀I:{I:Interval| icompact(I)} . ∀f,g:I^n1 ⟶ ℝ.
((∀x,y:I^n1. (req-vec(n1;x;y)
⇒ ((f x) = (f y))))
⇒ (∀x:I^n1. ((f x) = (g x)))
⇒ ((infn(n1;I) f) = (infn(n1;I) g))) ∈ ℙ)
⊢ ∀n:ℕ. ∀I:{I:Interval| icompact(I)} . ∀f,g:I^n ⟶ ℝ.
((∀x,y:I^n. (req-vec(n;x;y)
⇒ ((f x) = (f y))))
⇒ (∀x:I^n. ((f x) = (g x)))
⇒ ((infn(n;I) f) = (infn(n;I) g)))
Latex:
Latex:
No Annotations
\mforall{}n:\mBbbN{}. \mforall{}I:\{I:Interval| icompact(I)\} . \mforall{}f,g:I\^{}n {}\mrightarrow{} \mBbbR{}.
((\mforall{}x,y:I\^{}n. (req-vec(n;x;y) {}\mRightarrow{} ((f x) = (f y))))
{}\mRightarrow{} (\mforall{}x:I\^{}n. ((f x) = (g x)))
{}\mRightarrow{} ((infn(n;I) f) = (infn(n;I) g)))
By
Latex:
(Assert \mforall{}n1:\mBbbN{}
(\mforall{}I:\{I:Interval| icompact(I)\} . \mforall{}f,g:I\^{}n1 {}\mrightarrow{} \mBbbR{}.
((\mforall{}x,y:I\^{}n1. (req-vec(n1;x;y) {}\mRightarrow{} ((f x) = (f y))))
{}\mRightarrow{} (\mforall{}x:I\^{}n1. ((f x) = (g x)))
{}\mRightarrow{} ((infn(n1;I) f) = (infn(n1;I) g))) \mmember{} \mBbbP{}) BY
((D 0 THENA Auto)
THEN RepeatFor 5 ((MemCD THENL [Auto; Id]))
THEN (Assert \mforall{}x,y:I\^{}n1. (req-vec(n1;x;y) {}\mRightarrow{} ((g x) = (g y))) BY
(RWO "-1<" 0 THEN Auto))
THEN RepeatFor 2 (MemCD)
THEN Auto))
Home
Index