:: SEQFUNC semantic presentation

definition

let c₁, c₂ be set ;
mode Functional_Sequence of c₁,c₂ -> Function means :Def1: :: SEQFUNC:def 1
( dom a₃ = NAT & rng a₃ c= PFuncs a₁,a₂ );
existence

proof end;

end;

:: deftheorem Def1 defines Functional_Sequence SEQFUNC:def 1 :

definition

let c₁, c₂ be set ;
let c₃ be Functional_Sequence of c₁,c₂;
let c₄ be natural number ;
redefine func . as c₃ . c₄ -> PartFunc of a₁,a₂;
coherence

proof end;

end;

Lemma2: for b₁, b₂ being set
for b₃ being Function holds
( b₃ is Functional_Sequence of b₁,b₂ iff ( dom b₃ = NAT & ( for b₄ being set st b₄ in NAT holds
b₃ . b₄ is PartFunc of b₁,b₂ ) ) )

proof end;

theorem Th1: :: SEQFUNC:1

for b₁, b₂ being set
for b₃ being Function holds
( b₃ is Functional_Sequence of b₁,b₂ iff ( dom b₃ = NAT & ( for b₄ being Nat holds b₃ . b₄ is PartFunc of b₁,b₂ ) ) )

proof end;

Lemma3: for b₁, b₂ being set
for b₃, b₄ being Functional_Sequence of b₂,b₁ st ( for b₅ being set st b₅ in NAT holds
b₃ . b₅ = b₄ . b₅ ) holds
b₃ = b₄

proof end;

theorem Th2: :: SEQFUNC:2

for b₁, b₂ being set
for b₃, b₄ being Functional_Sequence of b₂,b₁ st ( for b₅ being Nat holds b₃ . b₅ = b₄ . b₅ ) holds
b₃ = b₄

proof end;

scheme :: SEQFUNC:sch 1
s1{ F₁() -> set , F₂() -> set , F₃( Nat) -> PartFunc of F₁(),F₂() } :

ex b₁ being Functional_Sequence of F₁(),F₂() st
for b₂ being Nat holds b₁ . b₂ = F₃(b₂)

proof end;

definition

let c₁ be non empty set ;
let c₂ be Functional_Sequence of c₁, REAL ;
let c₃ be real number ;
func c₃ (#) c₂ -> Functional_Sequence of a₁, REAL means :Def2: :: SEQFUNC:def 2
for b₁ being Nat holds a₄ . b₁ = a₃ (#) (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines (#) SEQFUNC:def 2 :

definition

let c₁ be non empty set ;
let c₂ be Functional_Sequence of c₁, REAL ;
func c₂ " -> Functional_Sequence of a₁, REAL means :Def3: :: SEQFUNC:def 3
for b₁ being Nat holds a₃ . b₁ = (a₂ . b₁) ^ ;
existence

proof end;

uniqueness

proof end;

func - c₂ -> Functional_Sequence of a₁, REAL means :Def4: :: SEQFUNC:def 4
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

func abs c₂ -> Functional_Sequence of a₁, REAL means :Def5: :: SEQFUNC:def 5
for b₁ being Nat holds a₃ . b₁ = abs (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines " SEQFUNC:def 3 :

:: deftheorem Def4 defines - SEQFUNC:def 4 :

:: deftheorem Def5 defines abs SEQFUNC:def 5 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Functional_Sequence of c₁, REAL ;
func c₂ + c₃ -> Functional_Sequence of a₁, REAL means :Def6: :: SEQFUNC:def 6
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + SEQFUNC:def 6 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Functional_Sequence of c₁, REAL ;
func c₂ - c₃ -> Functional_Sequence of a₁, REAL equals :: SEQFUNC:def 7
a₂ + (- a₃);
correctness ;

end;

:: deftheorem Def7 defines - SEQFUNC:def 7 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Functional_Sequence of c₁, REAL ;
func c₂ (#) c₃ -> Functional_Sequence of a₁, REAL means :Def8: :: SEQFUNC:def 8
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) (#) (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines (#) SEQFUNC:def 8 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Functional_Sequence of c₁, REAL ;
func c₃ / c₂ -> Functional_Sequence of a₁, REAL equals :: SEQFUNC:def 9
a₃ (#) (a₂ " );
correctness ;

end;

:: deftheorem Def9 defines / SEQFUNC:def 9 :

theorem Th3: :: SEQFUNC:3

for b₁ being non empty set
for b₂, b₃, b₄ being Functional_Sequence of b₁, REAL holds
( b₂ = b₃ / b₄ iff for b₅ being Nat holds b₂ . b₅ = (b₃ . b₅) / (b₄ . b₅) )

proof end;

theorem Th4: :: SEQFUNC:4

for b₁ being non empty set
for b₂, b₃, b₄ being Functional_Sequence of b₁, REAL holds
( b₂ = b₃ - b₄ iff for b₅ being Nat holds b₂ . b₅ = (b₃ . b₅) - (b₄ . b₅) )

proof end;

theorem Th5: :: SEQFUNC:5

for b₁ being non empty set
for b₂, b₃, b₄ being Functional_Sequence of b₁, REAL holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) )

proof end;

theorem Th6: :: SEQFUNC:6

for b₁ being non empty set
for b₂, b₃, b₄ being Functional_Sequence of b₁, REAL holds
( b₂ (#) b₃ = b₃ (#) b₂ & (b₂ (#) b₃) (#) b₄ = b₂ (#) (b₃ (#) b₄) )

proof end;

theorem Th7: :: SEQFUNC:7

for b₁ being non empty set
for b₂, b₃, b₄ being Functional_Sequence of b₁, REAL holds
( (b₂ + b₃) (#) b₄ = (b₂ (#) b₄) + (b₃ (#) b₄) & b₄ (#) (b₂ + b₃) = (b₄ (#) b₂) + (b₄ (#) b₃) )

proof end;

theorem Th8: :: SEQFUNC:8

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL holds - b₂ = (- 1) (#) b₂

proof end;

theorem Th9: :: SEQFUNC:9

for b₁ being non empty set
for b₂, b₃, b₄ being Functional_Sequence of b₁, REAL holds
( (b₂ - b₃) (#) b₄ = (b₂ (#) b₄) - (b₃ (#) b₄) & (b₄ (#) b₂) - (b₄ (#) b₃) = b₄ (#) (b₂ - b₃) )

proof end;

theorem Th10: :: SEQFUNC:10

for b₁ being non empty set
for b₂ being Real
for b₃, b₄ being Functional_Sequence of b₁, REAL holds
( b₂ (#) (b₃ + b₄) = (b₂ (#) b₃) + (b₂ (#) b₄) & b₂ (#) (b₃ - b₄) = (b₂ (#) b₃) - (b₂ (#) b₄) )

proof end;

theorem Th11: :: SEQFUNC:11

for b₁ being non empty set
for b₂, b₃ being Real
for b₄ being Functional_Sequence of b₁, REAL holds (b₂ * b₃) (#) b₄ = b₂ (#) (b₃ (#) b₄)

proof end;

theorem Th12: :: SEQFUNC:12

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL holds 1 (#) b₂ = b₂

proof end;

theorem Th13: :: SEQFUNC:13

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL holds - (- b₂) = b₂

proof end;

theorem Th14: :: SEQFUNC:14

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL holds (b₂ " ) (#) (b₃ " ) = (b₂ (#) b₃) "

proof end;

theorem Th15: :: SEQFUNC:15

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL st b₂ <> 0 holds
(b₂ (#) b₃) " = (b₂ " ) (#) (b₃ " )

proof end;

theorem Th16: :: SEQFUNC:16

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL holds (abs b₂) " = abs (b₂ " )

proof end;

theorem Th17: :: SEQFUNC:17

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL holds abs (b₂ (#) b₃) = (abs b₂) (#) (abs b₃)

proof end;

theorem Th18: :: SEQFUNC:18

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL holds abs (b₂ / b₃) = (abs b₂) / (abs b₃)

proof end;

theorem Th19: :: SEQFUNC:19

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL holds abs (b₂ (#) b₃) = (abs b₂) (#) (abs b₃)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Functional_Sequence of c₁,c₂;
let c₄ be set ;
pred c₄ common_on_dom c₃ means :Def10: :: SEQFUNC:def 10
( a₄ <> {} & ( for b₁ being Nat holds a₄ c= dom (a₃ . b₁) ) );

end;

:: deftheorem Def10 defines common_on_dom SEQFUNC:def 10 :

definition

let c₁ be non empty set ;
let c₂ be Functional_Sequence of c₁, REAL ;
let c₃ be Element of c₁;
func c₂ # c₃ -> Real_Sequence means :Def11: :: SEQFUNC:def 11
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) . a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines # SEQFUNC:def 11 :

definition

let c₁ be non empty set ;
let c₂ be Functional_Sequence of c₁, REAL ;
let c₃ be set ;
pred c₂ is_point_conv_on c₃ means :Def12: :: SEQFUNC:def 12
( a₃ common_on_dom a₂ & ex b₁ being PartFunc of a₁, REAL st
( a₃ = dom b₁ & ( for b₂ being Element of a₁ st b₂ in a₃ holds
for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
abs (((a₂ . b₅) . b₂) - (b₁ . b₂)) < b₃ ) ) );

end;

:: deftheorem Def12 defines is_point_conv_on SEQFUNC:def 12 :

theorem Th20: :: SEQFUNC:20

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set holds
( b₂ is_point_conv_on b₃ iff ( b₃ common_on_dom b₂ & ex b₄ being PartFunc of b₁, REAL st
( b₃ = dom b₄ & ( for b₅ being Element of b₁ st b₅ in b₃ holds
( b₂ # b₅ is convergent & lim (b₂ # b₅) = b₄ . b₅ ) ) ) ) )

proof end;

theorem Th21: :: SEQFUNC:21

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set holds
( b₂ is_point_conv_on b₃ iff ( b₃ common_on_dom b₂ & ( for b₄ being Element of b₁ st b₄ in b₃ holds
b₂ # b₄ is convergent ) ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Functional_Sequence of c₁, REAL ;
let c₃ be set ;
pred c₂ is_unif_conv_on c₃ means :Def13: :: SEQFUNC:def 13
( a₃ common_on_dom a₂ & ex b₁ being PartFunc of a₁, REAL st
( a₃ = dom b₁ & ( for b₂ being Real st b₂ > 0 holds
ex b₃ being Nat st
for b₄ being Nat
for b₅ being Element of a₁ st b₄ >= b₃ & b₅ in a₃ holds
abs (((a₂ . b₄) . b₅) - (b₁ . b₅)) < b₂ ) ) );

end;

:: deftheorem Def13 defines is_unif_conv_on SEQFUNC:def 13 :

definition

let c₁ be non empty set ;
let c₂ be Functional_Sequence of c₁, REAL ;
let c₃ be set ;
assume E24: c₂ is_point_conv_on c₃ ;
func lim c₂,c₃ -> PartFunc of a₁, REAL means :Def14: :: SEQFUNC:def 14
( dom a₄ = a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = lim (a₂ # b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines lim SEQFUNC:def 14 :

theorem Th22: :: SEQFUNC:22

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set
for b₄ being PartFunc of b₁, REAL st b₂ is_point_conv_on b₃ holds
( b₄ = lim b₂,b₃ iff ( dom b₄ = b₃ & ( for b₅ being Element of b₁ st b₅ in b₃ holds
for b₆ being Real st b₆ > 0 holds
ex b₇ being Nat st
for b₈ being Nat st b₈ >= b₇ holds
abs (((b₂ . b₈) . b₅) - (b₄ . b₅)) < b₆ ) ) )

proof end;

theorem Th23: :: SEQFUNC:23

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₂ is_unif_conv_on b₃ holds
b₂ is_point_conv_on b₃

proof end;

theorem Th24: :: SEQFUNC:24

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃, b₄ being set st b₃ c= b₄ & b₃ <> {} & b₄ common_on_dom b₂ holds
b₃ common_on_dom b₂

proof end;

theorem Th25: :: SEQFUNC:25

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃, b₄ being set st b₃ c= b₄ & b₃ <> {} & b₂ is_point_conv_on b₄ holds
( b₂ is_point_conv_on b₃ & (lim b₂,b₄) | b₃ = lim b₂,b₃ )

proof end;

theorem Th26: :: SEQFUNC:26

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃, b₄ being set st b₃ c= b₄ & b₃ <> {} & b₂ is_unif_conv_on b₄ holds
b₂ is_unif_conv_on b₃

proof end;

theorem Th27: :: SEQFUNC:27

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₃ common_on_dom b₂ holds
for b₄ being Element of b₁ st b₄ in b₃ holds
{b₄} common_on_dom b₂

proof end;

theorem Th28: :: SEQFUNC:28

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₂ is_point_conv_on b₃ holds
for b₄ being Element of b₁ st b₄ in b₃ holds
{b₄} common_on_dom b₂

proof end;

theorem Th29: :: SEQFUNC:29

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL
for b₄ being Element of b₁ st {b₄} common_on_dom b₂ & {b₄} common_on_dom b₃ holds
( (b₂ # b₄) + (b₃ # b₄) = (b₂ + b₃) # b₄ & (b₂ # b₄) - (b₃ # b₄) = (b₂ - b₃) # b₄ & (b₂ # b₄) (#) (b₃ # b₄) = (b₂ (#) b₃) # b₄ )

proof end;

theorem Th30: :: SEQFUNC:30

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being Element of b₁ st {b₃} common_on_dom b₂ holds
( (abs b₂) # b₃ = abs (b₂ # b₃) & (- b₂) # b₃ = - (b₂ # b₃) )

proof end;

theorem Th31: :: SEQFUNC:31

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL
for b₄ being Element of b₁ st {b₄} common_on_dom b₃ holds
(b₂ (#) b₃) # b₄ = b₂ (#) (b₃ # b₄)

proof end;

theorem Th32: :: SEQFUNC:32

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₄ common_on_dom b₂ & b₄ common_on_dom b₃ holds
for b₅ being Element of b₁ st b₅ in b₄ holds
( (b₂ # b₅) + (b₃ # b₅) = (b₂ + b₃) # b₅ & (b₂ # b₅) - (b₃ # b₅) = (b₂ - b₃) # b₅ & (b₂ # b₅) (#) (b₃ # b₅) = (b₂ (#) b₃) # b₅ )

proof end;

theorem Th33: :: SEQFUNC:33

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₃ common_on_dom b₂ holds
for b₄ being Element of b₁ st b₄ in b₃ holds
( (abs b₂) # b₄ = abs (b₂ # b₄) & (- b₂) # b₄ = - (b₂ # b₄) )

proof end;

theorem Th34: :: SEQFUNC:34

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₄ common_on_dom b₃ holds
for b₅ being Element of b₁ st b₅ in b₄ holds
(b₂ (#) b₃) # b₅ = b₂ (#) (b₃ # b₅)

proof end;

theorem Th35: :: SEQFUNC:35

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₂ is_point_conv_on b₄ & b₃ is_point_conv_on b₄ holds
for b₅ being Element of b₁ st b₅ in b₄ holds
( (b₂ # b₅) + (b₃ # b₅) = (b₂ + b₃) # b₅ & (b₂ # b₅) - (b₃ # b₅) = (b₂ - b₃) # b₅ & (b₂ # b₅) (#) (b₃ # b₅) = (b₂ (#) b₃) # b₅ )

proof end;

theorem Th36: :: SEQFUNC:36

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₂ is_point_conv_on b₃ holds
for b₄ being Element of b₁ st b₄ in b₃ holds
( (abs b₂) # b₄ = abs (b₂ # b₄) & (- b₂) # b₄ = - (b₂ # b₄) )

proof end;

theorem Th37: :: SEQFUNC:37

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₃ is_point_conv_on b₄ holds
for b₅ being Element of b₁ st b₅ in b₄ holds
(b₂ (#) b₃) # b₅ = b₂ (#) (b₃ # b₅)

proof end;

theorem Th38: :: SEQFUNC:38

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₄ common_on_dom b₂ & b₄ common_on_dom b₃ holds
( b₄ common_on_dom b₂ + b₃ & b₄ common_on_dom b₂ - b₃ & b₄ common_on_dom b₂ (#) b₃ )

proof end;

theorem Th39: :: SEQFUNC:39

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₃ common_on_dom b₂ holds
( b₃ common_on_dom abs b₂ & b₃ common_on_dom - b₂ )

proof end;

theorem Th40: :: SEQFUNC:40

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₄ common_on_dom b₃ holds
b₄ common_on_dom b₂ (#) b₃

proof end;

theorem Th41: :: SEQFUNC:41

for b₁ being non empty set
for b₂, b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₂ is_point_conv_on b₄ & b₃ is_point_conv_on b₄ holds
( b₂ + b₃ is_point_conv_on b₄ & lim (b₂ + b₃),b₄ = (lim b₂,b₄) + (lim b₃,b₄) & b₂ - b₃ is_point_conv_on b₄ & lim (b₂ - b₃),b₄ = (lim b₂,b₄) - (lim b₃,b₄) & b₂ (#) b₃ is_point_conv_on b₄ & lim (b₂ (#) b₃),b₄ = (lim b₂,b₄) (#) (lim b₃,b₄) )

proof end;

theorem Th42: :: SEQFUNC:42

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set st b₂ is_point_conv_on b₃ holds
( abs b₂ is_point_conv_on b₃ & lim (abs b₂),b₃ = abs (lim b₂,b₃) & - b₂ is_point_conv_on b₃ & lim (- b₂),b₃ = - (lim b₂,b₃) )

proof end;

theorem Th43: :: SEQFUNC:43

for b₁ being non empty set
for b₂ being Real
for b₃ being Functional_Sequence of b₁, REAL
for b₄ being set st b₃ is_point_conv_on b₄ holds
( b₂ (#) b₃ is_point_conv_on b₄ & lim (b₂ (#) b₃),b₄ = b₂ (#) (lim b₃,b₄) )

proof end;

theorem Th44: :: SEQFUNC:44

for b₁ being non empty set
for b₂ being Functional_Sequence of b₁, REAL
for b₃ being set holds
( b₂ is_unif_conv_on b₃ iff ( b₃ common_on_dom b₂ & b₂ is_point_conv_on b₃ & ( for b₄ being Real st 0 < b₄ holds
ex b₅ being Nat st
for b₆ being Nat
for b₇ being Element of b₁ st b₆ >= b₅ & b₇ in b₃ holds
abs (((b₂ . b₆) . b₇) - ((lim b₂,b₃) . b₇)) < b₄ ) ) )

proof end;

theorem Th45: :: SEQFUNC:45

for b₁ being set
for b₂ being Functional_Sequence of REAL , REAL st b₂ is_unif_conv_on b₁ & ( for b₃ being Nat holds b₂ . b₃ is_continuous_on b₁ ) holds
lim b₂,b₁ is_continuous_on b₁

proof end;