:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama

::

:: Received February 22, 2011

:: Copyright (c) 2011-2012 Association of Mizar Users

begin

definition

let n be Element of NAT ;

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

let x0 be real number ;

end;
let f be PartFunc of REAL,(REAL n);

let x0 be real number ;

pred f is_continuous_in x0 means :Def1: :: NFCONT_4:def 1

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_continuous_in x0 );

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_continuous_in x0 );

:: deftheorem Def1 defines is_continuous_in NFCONT_4:def 1 :

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

for x0 being real number holds

( f is_continuous_in x0 iff ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_continuous_in x0 ) );

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

for x0 being real number holds

( f is_continuous_in x0 iff ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_continuous_in x0 ) );

theorem Th1: :: NFCONT_4:1

for n being Element of NAT

for x0 being real number

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 )

for x0 being real number

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 )

proof end;

theorem Th2: :: NFCONT_4:2

for n being Element of NAT

for X being set

for x0 being real number

for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds

f | X is_continuous_in x0

for X being set

for x0 being real number

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 number

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 number st

( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

for x0 being real number

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 number st

( 0 < s & ( for x1 being real number st x1 in dom f & abs (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 }

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_{1}( set ) -> Element of REAL = |.(f /. $1).|;

ex b_{1} being PartFunc of Z,REAL st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} /. x = |.(f /. x).| ) )

for b_{1}, b_{2} being PartFunc of Z,REAL st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} /. x = |.(f /. x).| ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} /. x = |.(f /. x).| ) holds

b_{1} = b_{2}

end;
let Z be set ;

let f be PartFunc of Z,(REAL n);

deffunc H

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 ( dom it = dom f & ( for x being set st x in dom it holds

it /. x = |.(f /. x).| ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for n being Element of NAT

for Z being set

for f being PartFunc of Z,(REAL n)

for b_{4} being PartFunc of Z,REAL holds

( b_{4} = |.f.| iff ( dom b_{4} = dom f & ( for x being set st x in dom b_{4} holds

b_{4} /. x = |.(f /. x).| ) ) );

for n being Element of NAT

for Z being set

for f being PartFunc of Z,(REAL n)

for b

( b

b

definition

let n be Element of NAT ;

let Z be non empty set ;

let f be PartFunc of Z,(REAL n);

deffunc H_{1}( set ) -> M13( REAL , REAL n) = - (f /. $1);

defpred S_{1}[ set ] means $1 in dom f;

ex b_{1} being PartFunc of Z,(REAL n) st

( dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} /. c = - (f /. c) ) )

for b_{1}, b_{2} being PartFunc of Z,(REAL n) st dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} /. c = - (f /. c) ) & dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} /. c = - (f /. c) ) holds

b_{1} = b_{2}

end;
let Z be non empty set ;

let f be PartFunc of Z,(REAL n);

deffunc H

defpred S

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 ( dom it = dom f & ( for c being set st c in dom it holds

it /. c = - (f /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines - NFCONT_4:def 3 :

for n being Element of NAT

for Z being non empty set

for f, b_{4} being PartFunc of Z,(REAL n) holds

( b_{4} = - f iff ( dom b_{4} = dom f & ( for c being set st c in dom b_{4} holds

b_{4} /. c = - (f /. c) ) ) );

for n being Element of NAT

for Z being non empty set

for f, b

( b

b

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

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

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 :: NFCONT_4:7

for n being Element of NAT

for W being non empty set

for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1

for W being non empty set

for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1

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

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.|

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

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 number

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 number st x1 in dom f & x1 in N holds

f /. x1 in N1 ) ) )

for x0 being real number

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 number st x1 in dom f & x1 in N holds

f /. x1 in N1 ) ) )

proof end;

theorem :: NFCONT_4:12

for n being Element of NAT

for x0 being real number

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 f .: N c= N1 ) ) )

for x0 being real number

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 f .: N c= N1 ) ) )

proof end;

theorem :: NFCONT_4:13

for n being Element of NAT

for x0 being real number

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

for x0 being real number

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 number

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

for x0 being real number

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 number

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

for x0 being real number

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 being Real

for x0 being real number

for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

for r being Real

for x0 being real number

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 number

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

|.f.| is_continuous_in x0

for x0 being real number

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 number

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

- f is_continuous_in x0

for x0 being real number

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 number

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

for x0 being real number

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 number

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

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;

end;
let f be PartFunc of (REAL n),REAL;

let x0 be Element of REAL n;

pred f is_continuous_in x0 means :Def4: :: 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 );

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 );

:: deftheorem Def4 defines is_continuous_in NFCONT_4:def 4 :

for n being Element of NAT

for f being PartFunc of (REAL n),REAL

for x0 being Element of REAL n holds

( f is_continuous_in x0 iff 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 ) );

for n being Element of NAT

for f being PartFunc of (REAL n),REAL

for x0 being Element of REAL n holds

( f is_continuous_in x0 iff 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 ) );

theorem Th21: :: 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 )

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 )

proof end;

theorem Th22: :: NFCONT_4:22

for n being Element of NAT

for x0 being real number

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

for x0 being real number

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);

end;
let f be PartFunc of REAL,(REAL n);

attr f is continuous means :Def5: :: NFCONT_4:def 5

for x0 being real number st x0 in dom f holds

f is_continuous_in x0;

for x0 being real number st x0 in dom f holds

f is_continuous_in x0;

:: deftheorem Def5 defines continuous NFCONT_4:def 5 :

for n being Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is continuous iff for x0 being real number st x0 in dom f holds

f is_continuous_in x0 );

for n being Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is continuous iff for x0 being real number st x0 in dom f holds

f is_continuous_in x0 );

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 )

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 being real number

for r being Real st x0 in X & 0 < r holds

ex s being real number st

( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) )

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 being real number

for r being Real st x0 in X & 0 < r holds

ex s being real number st

( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) )

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} is constant holds

b_{1} is continuous

end;
coherence

for b

b

proof end;

registration

let n be Element of NAT ;

ex b_{1} being PartFunc of REAL,(REAL n) st b_{1} is continuous

end;
cluster Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() continuous for Element of bool [:REAL,(REAL n):];

existence ex b

proof end;

registration

let n be Element of NAT ;

let f be continuous PartFunc of REAL,(REAL n);

let X be set ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = f | X holds

b_{1} is continuous

end;
let f be continuous PartFunc of REAL,(REAL n);

let X be set ;

coherence

for b

b

proof 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

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 ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} is empty holds

b_{1} is continuous
;

end;
coherence

for b

b

registration

let n be Element of NAT ;

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

let X be trivial set ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = f | X holds

b_{1} is continuous

end;
let f be PartFunc of REAL,(REAL n);

let X be trivial set ;

coherence

for b

b

proof end;

registration

let n be Element of NAT ;

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

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = f1 + f2 holds

b_{1} is continuous

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

coherence

for b

b

proof 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 )

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 )

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;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = r (#) f holds

b_{1} is continuous

end;
let f be continuous PartFunc of REAL,(REAL n);

let r be Real;

coherence

for b

b

proof 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

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

for n being Element of NAT

for X being set

for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds

( |.f.| | X is continuous & (- f) | X is continuous )

for X being set

for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds

( |.f.| | X is continuous & (- f) | X is continuous )

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 number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds

f | REAL is continuous

for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number 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

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

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);

end;
let f be PartFunc of REAL,(REAL n);

attr f is Lipschitzian means :Def6: :: NFCONT_4:def 6

ex g being PartFunc of REAL,(REAL-NS n) st

( g = f & g is Lipschitzian );

ex g being PartFunc of REAL,(REAL-NS n) st

( g = f & g is Lipschitzian );

:: deftheorem Def6 defines Lipschitzian NFCONT_4:def 6 :

for n being Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is Lipschitzian iff ex g being PartFunc of REAL,(REAL-NS n) st

( g = f & g is Lipschitzian ) );

for n being Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is Lipschitzian iff ex g being PartFunc of REAL,(REAL-NS n) st

( g = f & g is Lipschitzian ) );

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 number st

( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds

|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )

for f being PartFunc of REAL,(REAL n) holds

( f is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds

|.((f /. x1) - (f /. x2)).| <= r * (abs (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 )

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 )

proof end;

theorem :: NFCONT_4:35

for n being Element of NAT

for X being set

for f being PartFunc of REAL,(REAL n) holds

( f | X is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds

|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )

for X being set

for f being PartFunc of REAL,(REAL n) holds

( f | X is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds

|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} is empty holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

registration

let n be Element of NAT ;

ex b_{1} being PartFunc of REAL,(REAL n) st b_{1} is empty

end;
cluster empty Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() for Element of bool [:REAL,(REAL n):];

existence ex b

proof end;

registration

let n be Element of NAT ;

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

let X be set ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = f | X holds

b_{1} is Lipschitzian

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

let X be set ;

coherence

for b

b

proof 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

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);

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = f1 + f2 holds

b_{1} is Lipschitzian

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = f1 - f2 holds

b_{1} is Lipschitzian

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

coherence

for b

b

proof end;

coherence for b

b

proof 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

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

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;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} = p (#) f holds

b_{1} is Lipschitzian

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

let p be Real;

coherence

for b

b

proof 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

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);

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = |.f.| holds

b_{1} is Lipschitzian

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

coherence

for b

b

proof end;

theorem :: NFCONT_4:40

for n being Element of NAT

for X being set

for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )

for X being set

for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} is constant holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being PartFunc of REAL,(REAL n) st b_{1} is Lipschitzian holds

b_{1} is continuous

end;
coherence

for b

b

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 number st x0 in X holds

f /. x0 = (x0 * r) + p ) holds

f | X is continuous

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 number 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

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 number

for n being non empty 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 ) ) )

for n being non empty 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 empty 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 )

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

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 number

for n being non empty 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 )

for n being non empty 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 empty 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 )

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;