HEINE

:: HEINE semantic presentation

for x, y being ( ( real ) ( V14() real ext-real ) number )
for A being ( ( ) ( Reflexive discerning V146() triangle ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V146() triangle Discerning ) MetrStruct ) )
for p, q being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x : ( ( real ) ( V14() real ext-real ) number ) = p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) & y : ( ( real ) ( V14() real ext-real ) number ) = q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
dist (p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V14() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) = abs (x : ( ( real ) ( V14() real ext-real ) number ) - y : ( ( real ) ( V14() real ext-real ) number ) ) : ( ( ) ( V14() real ext-real ) set ) : ( ( ) ( V14() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ;

theorem :: HEINE:2

for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) )
for seq being ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is V40() & rng seq : ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V51() V52() V53() ) set ) c= NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) holds
n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= seq : ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V14() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ;

definition

let seq be ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ;
let k be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

func k to_power seq -> ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) means :: HEINE:def 1
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) Element of seq : ( ( ) ( ) TopStruct ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V14() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) = k : ( ( ) ( ) Element of K10(K10(seq : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) to_power (seq : ( ( ) ( ) TopStruct ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V14() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( V14() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ;

end;

theorem :: HEINE:3

for seq being ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty holds
2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V49() V50() V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) to_power seq : ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V24() V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) -valued V24() V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K10(REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial V51() V52() V53() V57() non finite ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty ;

theorem :: HEINE:4

for a, b being ( ( real ) ( V14() real ext-real ) number ) st a : ( ( real ) ( V14() real ext-real ) number ) <= b : ( ( real ) ( V14() real ext-real ) number ) holds
Closed-Interval-TSpace (a : ( ( real ) ( V14() real ext-real ) number ) ,b : ( ( real ) ( V14() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like ) SubSpace of R^1 : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) is compact ;