NFCONT_4: More on the Continuity of Real Functions

definition

let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let x0 be Real;

pred f is_continuous_in x0 means :: NFCONT_4:def 1
ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 );

end;

:: deftheorem defines is_continuous_in NFCONT_4:def 1 :

theorem :: NFCONT_4:1

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 ) ;

theorem Th2: :: NFCONT_4:2

for n being Element of NAT
for X being set
for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0

proof end;

theorem Th3: :: NFCONT_4:3

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

theorem Th4: :: NFCONT_4:4

for n being Element of NAT
for r being Real
for z being Element of REAL n
for w being Point of (REAL-NS n) st z = w holds
{ y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }

proof end;

definition

let n be Element of NAT ;
let Z be set ;
let f be PartFunc of Z,(REAL n);
deffunc H₁( object ) -> object = |.(f /. $1).|;

func |.f.| -> PartFunc of Z,REAL means :Def2: :: NFCONT_4:def 2
( dom it = dom f & ( for x being set st x in dom it holds
it /. x = |.(f /. x).| ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines |. NFCONT_4:def 2 :

definition

let n be Element of NAT ;
let Z be non empty set ;
let f be PartFunc of Z,(REAL n);
deffunc H₁( set ) -> M14( REAL , REAL n) = - (f /. $1);
defpred S₁[ set ] means $1 in dom f;

func - f -> PartFunc of Z,(REAL n) means :Def3: :: NFCONT_4:def 3
( dom it = dom f & ( for c being set st c in dom it holds
it /. c = - (f /. c) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines - NFCONT_4:def 3 :

theorem Th5: :: NFCONT_4:5

for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2

proof end;

theorem Th6: :: NFCONT_4:6

for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1

proof end;

theorem Th8: :: NFCONT_4:8

for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1

proof end;

theorem Th9: :: NFCONT_4:9

for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|

proof end;

theorem Th10: :: NFCONT_4:10

for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2

proof end;

theorem :: NFCONT_4:11

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )

proof end;

theorem :: NFCONT_4:12

proof end;

theorem :: NFCONT_4:13

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0

proof end;

theorem :: NFCONT_4:14

for n being Element of NAT
for x0 being Real
for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 + f2 is_continuous_in x0

proof end;

theorem :: NFCONT_4:15

for n being Element of NAT
for x0 being Real
for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 - f2 is_continuous_in x0

proof end;

theorem :: NFCONT_4:16

for n being Element of NAT
for r, x0 being Real
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0

proof end;

theorem :: NFCONT_4:17

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0

proof end;

theorem :: NFCONT_4:18

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
- f is_continuous_in x0

proof end;

theorem :: NFCONT_4:19

for n being Element of NAT
for x0 being Real
for S being RealNormSpace
for z being Point of (REAL-NS n)
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0

proof end;

theorem Th20: :: NFCONT_4:20

for x0 being Real
for S being RealNormSpace
for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0

proof end;

definition

let n be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x0 be Element of REAL n;

pred f is_continuous_in x0 means :: NFCONT_4:def 4
ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y0 & f = g & g is_continuous_in y0 );

end;

:: deftheorem defines is_continuous_in NFCONT_4:def 4 :

theorem :: NFCONT_4:21

for n being Element of NAT
for f being PartFunc of (REAL n),REAL
for h being PartFunc of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 ) ;

theorem Th22: :: NFCONT_4:22

for n being Element of NAT
for x0 being Real
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0

proof end;

definition

let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);

attr f is continuous means :Def5: :: NFCONT_4:def 5
for x0 being Real st x0 in dom f holds
f is_continuous_in x0;

end;

:: deftheorem Def5 defines continuous NFCONT_4:def 5 :

theorem Th23: :: NFCONT_4:23

for n being Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )

proof end;

theorem Th24: :: NFCONT_4:24

for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) st X c= dom f holds
( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )

proof end;

registration

let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let X be set ;

cluster f | X -> continuous for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

theorem :: NFCONT_4:25

for n being Element of NAT
for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds
f | X1 is continuous

proof end;

registration

let n be Element of NAT ;

cluster empty Function-like -> continuous for Element of bool [:REAL,(REAL n):];

coherence ;

end;

registration

let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let X be trivial set ;

cluster f | X -> continuous for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

registration

let n be Element of NAT ;
let f1, f2 be continuous PartFunc of REAL,(REAL n);

cluster f1 + f2 -> continuous for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

theorem :: NFCONT_4:26

for n being Element of NAT
for X being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )

proof end;

theorem :: NFCONT_4:27

for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )

proof end;

registration

let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let r be Real;

cluster r (#) f -> continuous for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

theorem :: NFCONT_4:28

for n being Element of NAT
for X being set
for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous

proof end;

theorem :: NFCONT_4:29

proof end;

theorem :: NFCONT_4:30

for n being Element of NAT
for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 holds
f | REAL is continuous

proof end;

theorem :: NFCONT_4:31

for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds
Y is compact

proof end;

theorem :: NFCONT_4:32

for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of REAL
for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact

proof end;

definition

let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);

attr f is Lipschitzian means :: NFCONT_4:def 6
ex g being PartFunc of REAL,(REAL-NS n) st
( g = f & g is Lipschitzian );

end;

:: deftheorem defines Lipschitzian NFCONT_4:def 6 :

theorem Th33: :: NFCONT_4:33

for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) )

proof end;

theorem Th34: :: NFCONT_4:34

for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian ) ;

theorem :: NFCONT_4:35

proof end;

registration

let n be Element of NAT ;

cluster empty Function-like -> Lipschitzian for Element of bool [:REAL,(REAL n):];

coherence

proof end;

end;

registration

let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let X be set ;

cluster f | X -> Lipschitzian for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

theorem :: NFCONT_4:36

for n being Element of NAT
for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian

proof end;

registration

let n be Element of NAT ;
let f1, f2 be Lipschitzian PartFunc of REAL,(REAL n);

cluster f1 + f2 -> Lipschitzian for PartFunc of REAL,(REAL n);

coherence

proof end;

cluster f1 - f2 -> Lipschitzian for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

theorem :: NFCONT_4:37

for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian

proof end;

theorem :: NFCONT_4:38

for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian

proof end;

registration

let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let p be Real;

cluster p (#) f -> Lipschitzian for PartFunc of REAL,(REAL n);

coherence

proof end;

end;

theorem :: NFCONT_4:39

for n being Element of NAT
for X being set
for p being Real
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian

proof end;

registration

let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);

cluster |.f.| -> Lipschitzian for PartFunc of REAL,REAL;

coherence

proof end;

end;

theorem :: NFCONT_4:40

proof end;

theorem :: NFCONT_4:41

for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being Real st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous

proof end;

theorem Th42: :: NFCONT_4:42

for n, i being Element of NAT
for x0 being Element of REAL n st 1 <= i & i <= n holds
proj (i,n) is_continuous_in x0

proof end;

theorem Th43: :: NFCONT_4:43

for x0 being Real
for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )

proof end;

theorem :: NFCONT_4:44

for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous )

proof end;

theorem Th45: :: NFCONT_4:45

for n, i being Element of NAT
for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds
Proj (i,n) is_continuous_in x0

proof end;

theorem Th46: :: NFCONT_4:46

for x0 being Real
for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )

proof end;

theorem :: NFCONT_4:47

for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )

proof end;