:: NFCONT_4 semantic presentation
begin
definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let x0 be real number ;
predf 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 );
end;
:: 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 ) );
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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let x0 be real number ; ::_thesis: 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 )
let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h = f implies ( f is_continuous_in x0 iff h is_continuous_in x0 ) )
assume A1: h = f ; ::_thesis: ( f is_continuous_in x0 iff h is_continuous_in x0 )
hereby ::_thesis: ( h is_continuous_in x0 implies f is_continuous_in x0 )
assume f is_continuous_in x0 ; ::_thesis: h is_continuous_in x0
then ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 ) by Def1;
hence h is_continuous_in x0 by A1; ::_thesis: verum
end;
thus ( h is_continuous_in x0 implies f is_continuous_in x0 ) by A1, Def1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let X be set ; ::_thesis: 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
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
A1: x0 in X and
A2: f is_continuous_in x0 ; ::_thesis: f | X is_continuous_in x0
consider g being PartFunc of REAL,(REAL-NS n) such that
A3: ( f = g & g is_continuous_in x0 ) by A2, Def1;
g | X is_continuous_in x0 by A1, A3, NFCONT_3:6;
hence f | X is_continuous_in x0 by A3, Def1; ::_thesis: verum
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 ) ) ) ) )
proof
let n be Element of NAT ; ::_thesis: 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 ) ) ) ) )
let x0 be real number ; ::_thesis: 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 ) ) ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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 ) ) ) ) )
hereby ::_thesis: ( 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 ) ) ) implies f is_continuous_in x0 )
assume f is_continuous_in x0 ; ::_thesis: ( 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 ) ) ) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_continuous_in x0 ) by Def1;
thus x0 in dom f by A1, NFCONT_3:8; ::_thesis: 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 ) )
thus 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 ) ) ::_thesis: verum
proof
let r be Real; ::_thesis: ( 0 < r implies 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 ) ) )
assume 0 < r ; ::_thesis: 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 ) )
then consider s being real number such that
A2: ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) ) by A1, NFCONT_3:8;
take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s by A2; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume ( x1 in dom f & abs (x1 - x0) < s ) ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
then A3: ||.((g /. x1) - (g /. x0)).|| < r by A1, A2;
( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by A1, REAL_NS1:def_4;
hence |.((f /. x1) - (f /. x0)).| < r by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
end;
assume A4: ( 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 ) ) ) ) ; ::_thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_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_g_&_abs_(x1_-_x0)_<_s_holds_
||.((g_/._x1)_-_(g_/._x0)).||_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) ) )
assume 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) )
then consider s being real number such that
A5: 0 < s and
A6: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r by A4;
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) )
thus 0 < s by A5; ::_thesis: for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r
let x1 be real number ; ::_thesis: ( x1 in dom g & abs (x1 - x0) < s implies ||.((g /. x1) - (g /. x0)).|| < r )
assume ( x1 in dom g & abs (x1 - x0) < s ) ; ::_thesis: ||.((g /. x1) - (g /. x0)).|| < r
then A7: |.((f /. x1) - (f /. x0)).| < r by A6;
( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by REAL_NS1:def_4;
hence ||.((g /. x1) - (g /. x0)).|| < r by A7, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
then g is_continuous_in x0 by A4, NFCONT_3:8;
hence f is_continuous_in x0 by Def1; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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 }
let r be Real; ::_thesis: 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 }
let z be Element of REAL n; ::_thesis: 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 }
let w be Point of (REAL-NS n); ::_thesis: ( z = w implies { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } )
assume A1: z = w ; ::_thesis: { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }
set N1 = { y where y is Element of REAL n : |.(y - z).| < r } ;
set N2 = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ;
A2: { y where y is Element of REAL n : |.(y - z).| < r } c= { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Element of REAL n : |.(y - z).| < r } or x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } )
assume x in { y where y is Element of REAL n : |.(y - z).| < r } ; ::_thesis: x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }
then consider y being Element of REAL n such that
A3: ( x = y & |.(y - z).| < r ) ;
reconsider x1 = x as Element of REAL n by A3;
reconsider x2 = x1 as Point of (REAL-NS n) by REAL_NS1:def_4;
||.(x2 - w).|| < r by A1, A3, REAL_NS1:1, REAL_NS1:5;
hence x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; ::_thesis: verum
end;
{ y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } c= { y where y is Element of REAL n : |.(y - z).| < r }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } or x in { y where y is Element of REAL n : |.(y - z).| < r } )
assume x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; ::_thesis: x in { y where y is Element of REAL n : |.(y - z).| < r }
then consider y being Point of (REAL-NS n) such that
A4: ( x = y & ||.(y - w).|| < r ) ;
reconsider x3 = x as Point of (REAL-NS n) by A4;
reconsider x4 = x3 as Element of REAL n by REAL_NS1:def_4;
|.(x4 - z).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5;
hence x in { y where y is Element of REAL n : |.(y - z).| < r } ; ::_thesis: verum
end;
hence { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let Z be set ;
let f be PartFunc of Z,(REAL n);
deffunc H1( set ) -> Element of REAL = |.(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
ex b1 being PartFunc of Z,REAL st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) )
proof
consider g being Function such that
A1: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
now__::_thesis:_for_y_being_set_st_y_in_rng_g_holds_
y_in_REAL
let y be set ; ::_thesis: ( y in rng g implies y in REAL )
assume y in rng g ; ::_thesis: y in REAL
then consider x being set such that
A2: ( x in dom g & y = g . x ) by FUNCT_1:def_3;
g . x = H1(x) by A1, A2;
hence y in REAL by A2; ::_thesis: verum
end;
then rng g c= REAL by TARSKI:def_3;
then g in PFuncs (Z,REAL) by A1, PARTFUN1:def_3;
then reconsider g = g as PartFunc of Z,REAL by PARTFUN1:46;
take g ; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds
g /. x = |.(f /. x).| ) )
thus dom g = dom f by A1; ::_thesis: for x being set st x in dom g holds
g /. x = |.(f /. x).|
let x be set ; ::_thesis: ( x in dom g implies g /. x = |.(f /. x).| )
assume A3: x in dom g ; ::_thesis: g /. x = |.(f /. x).|
then g . x = H1(x) by A1;
hence g /. x = |.(f /. x).| by A3, PARTFUN1:def_6; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of Z,REAL st dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) & dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 /. x = |.(f /. x).| ) holds
b1 = b2
proof
let g1, g2 be PartFunc of Z,REAL; ::_thesis: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = |.(f /. x).| ) & dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = |.(f /. x).| ) implies g1 = g2 )
assume that
A4: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = H1(x) ) ) and
A5: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = H1(x) ) ) ; ::_thesis: g1 = g2
now__::_thesis:_for_x_being_Element_of_Z_st_x_in_dom_g1_holds_
g1_._x_=_g2_._x
let x be Element of Z; ::_thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A6: x in dom g1 ; ::_thesis: g1 . x = g2 . x
then A7: g1 /. x = |.(f /. x).| by A4;
g1 /. x = g2 /. x by A5, A7, A4, A6;
then g1 . x = g2 /. x by A6, PARTFUN1:def_6;
hence g1 . x = g2 . x by A4, A5, A6, PARTFUN1:def_6; ::_thesis: verum
end;
hence g1 = g2 by A4, A5, PARTFUN1:5; ::_thesis: verum
end;
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 b4 being PartFunc of Z,REAL holds
( b4 = |.f.| iff ( dom b4 = dom f & ( for x being set st x in dom b4 holds
b4 /. x = |.(f /. x).| ) ) );
definition
let n be Element of NAT ;
let Z be non empty set ;
let f be PartFunc of Z,(REAL n);
deffunc H1( set ) -> M13( REAL , REAL n) = - (f /. $1);
defpred S1[ 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
ex b1 being PartFunc of Z,(REAL n) st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) )
proof
consider F being PartFunc of Z,(REAL n) such that
A1: for c being Element of Z holds
( c in dom F iff S1[c] ) and
A2: for c being Element of Z st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take F ; ::_thesis: ( dom F = dom f & ( for c being set st c in dom F holds
F /. c = - (f /. c) ) )
thus ( dom F = dom f & ( for c being set st c in dom F holds
F /. c = - (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 /. c = - (f /. c) ) holds
b1 = b2
proof
let g1, g2 be PartFunc of Z,(REAL n); ::_thesis: ( dom g1 = dom f & ( for c being set st c in dom g1 holds
g1 /. c = - (f /. c) ) & dom g2 = dom f & ( for c being set st c in dom g2 holds
g2 /. c = - (f /. c) ) implies g1 = g2 )
assume that
A3: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = - (f /. x) ) ) and
A4: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = - (f /. x) ) ) ; ::_thesis: g1 = g2
now__::_thesis:_for_x_being_Element_of_Z_st_x_in_dom_g1_holds_
g1_._x_=_g2_._x
let x be Element of Z; ::_thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A5: x in dom g1 ; ::_thesis: g1 . x = g2 . x
then A6: g1 /. x = - (f /. x) by A3;
g1 /. x = g2 /. x by A4, A6, A3, A5;
then g1 . x = g2 /. x by A5, PARTFUN1:def_6;
hence g1 . x = g2 . x by A3, A4, A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence g1 = g2 by A3, A4, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines - NFCONT_4:def_3_:_
for n being Element of NAT
for Z being non empty set
for f, b4 being PartFunc of Z,(REAL n) holds
( b4 = - f iff ( dom b4 = dom f & ( for c being set st c in dom b4 holds
b4 /. c = - (f /. c) ) ) );
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
let n be Element of NAT ; ::_thesis: 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
let W be non empty set ; ::_thesis: 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
let f1, f2 be PartFunc of W,(REAL-NS n); ::_thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2
A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1;
then A3: dom (f1 + f2) = dom (g1 + g2) by A1, VALUED_2:def_45;
A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_._x_=_(g1_+_g2)_._x
let x be Element of W; ::_thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (g1 + g2) . x )
assume A5: x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x = (g1 + g2) . x
then A6: ( x in dom g1 & x in dom g2 ) by A2, A1, XBOOLE_0:def_4;
A7: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def_4;
( g1 /. x = g1 . x & g2 /. x = g2 . x ) by A6, PARTFUN1:def_6;
then A8: (f1 /. x) + (f2 /. x) = (g1 . x) + (g2 . x) by A7, REAL_NS1:2;
(f1 + f2) /. x = (f1 /. x) + (f2 /. x) by A5, VFUNCT_1:def_1;
then (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A5, PARTFUN1:def_6;
hence (f1 + f2) . x = (g1 + g2) . x by A8, A3, A5, VALUED_2:def_45; ::_thesis: verum
end;
f1 + f2 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence f1 + f2 = g1 + g2 by A3, A4, PARTFUN1:5; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let W be non empty set ; ::_thesis: 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
let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let g1 be PartFunc of W,(REAL n); ::_thesis: for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let a be Real; ::_thesis: ( f1 = g1 implies a (#) f1 = a (#) g1 )
assume A1: f1 = g1 ; ::_thesis: a (#) f1 = a (#) g1
A2: dom (a (#) f1) = dom f1 by VFUNCT_1:def_4;
then A3: dom (a (#) f1) = dom (a (#) g1) by A1, VALUED_2:def_39;
A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(a_(#)_f1)_holds_
(a_(#)_f1)_._x_=_(a_(#)_g1)_._x
let x be Element of W; ::_thesis: ( x in dom (a (#) f1) implies (a (#) f1) . x = (a (#) g1) . x )
assume A5: x in dom (a (#) f1) ; ::_thesis: (a (#) f1) . x = (a (#) g1) . x
then A6: g1 . x = g1 /. x by A1, A2, PARTFUN1:def_6;
f1 /. x = g1 /. x by A1, REAL_NS1:def_4;
then A7: a * (f1 /. x) = a * (g1 /. x) by REAL_NS1:3;
A8: (a (#) f1) /. x = a * (f1 /. x) by A5, VFUNCT_1:def_4;
(a (#) g1) . x = a (#) (g1 . x) by A3, A5, VALUED_2:def_39;
hence (a (#) f1) . x = (a (#) g1) . x by A5, A7, A8, A6, PARTFUN1:def_6; ::_thesis: verum
end;
a (#) f1 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence a (#) f1 = a (#) g1 by A3, A4, PARTFUN1:5; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
let f1 be PartFunc of W,(REAL n); ::_thesis: (- 1) (#) f1 = - f1
A1: dom ((- 1) (#) f1) = dom f1 by VALUED_2:def_39;
then A2: dom ((- 1) (#) f1) = dom (- f1) by Def3;
now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_((-_1)_(#)_f1)_holds_
((-_1)_(#)_f1)_._x_=_(-_f1)_._x
let x be Element of W; ::_thesis: ( x in dom ((- 1) (#) f1) implies ((- 1) (#) f1) . x = (- f1) . x )
assume A3: x in dom ((- 1) (#) f1) ; ::_thesis: ((- 1) (#) f1) . x = (- f1) . x
A4: f1 . x = f1 /. x by A1, A3, PARTFUN1:def_6;
A5: (- f1) /. x = - (f1 /. x) by A2, A3, Def3;
(f1 [#] (- 1)) . x = (- 1) (#) (f1 . x) by A3, VALUED_2:def_39;
hence ((- 1) (#) f1) . x = (- f1) . x by A4, A2, A3, A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence (- 1) (#) f1 = - f1 by A2, PARTFUN1:5; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let g1 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 implies - f1 = - g1 )
assume A1: f1 = g1 ; ::_thesis: - f1 = - g1
dom (- f1) = dom f1 by VFUNCT_1:def_5;
then A2: dom (- f1) = dom (- g1) by A1, Def3;
A3: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(-_f1)_holds_
(-_f1)_._x_=_(-_g1)_._x
let x be Element of W; ::_thesis: ( x in dom (- f1) implies (- f1) . x = (- g1) . x )
assume A4: x in dom (- f1) ; ::_thesis: (- f1) . x = (- g1) . x
f1 /. x = g1 /. x by A1, REAL_NS1:def_4;
then A5: - (f1 /. x) = - (g1 /. x) by REAL_NS1:4;
A6: (- f1) /. x = - (f1 /. x) by A4, VFUNCT_1:def_5;
(- g1) /. x = - (g1 /. x) by A2, A4, Def3;
then (- f1) . x = (- g1) /. x by A4, A5, A6, PARTFUN1:def_6;
hence (- f1) . x = (- g1) . x by A2, A4, PARTFUN1:def_6; ::_thesis: verum
end;
- f1 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence - f1 = - g1 by A2, A3, PARTFUN1:5; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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.|
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let g1 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 implies ||.f1.|| = |.g1.| )
assume A1: f1 = g1 ; ::_thesis: ||.f1.|| = |.g1.|
dom ||.f1.|| = dom f1 by NORMSP_0:def_3;
then A2: dom ||.f1.|| = dom |.g1.| by A1, Def2;
now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_||.f1.||_holds_
||.f1.||_._x_=_|.g1.|_._x
let x be Element of W; ::_thesis: ( x in dom ||.f1.|| implies ||.f1.|| . x = |.g1.| . x )
assume A3: x in dom ||.f1.|| ; ::_thesis: ||.f1.|| . x = |.g1.| . x
A4: f1 /. x = g1 /. x by A1, REAL_NS1:def_4;
set y1 = g1 /. x;
A5: ||.(f1 /. x).|| = |.(g1 /. x).| by A4, REAL_NS1:1;
A6: ||.f1.|| . x = ||.(f1 /. x).|| by A3, NORMSP_0:def_3;
|.g1.| /. x = |.(g1 /. x).| by A2, A3, Def2;
hence ||.f1.|| . x = |.g1.| . x by A2, A3, A5, A6, PARTFUN1:def_6; ::_thesis: verum
end;
hence ||.f1.|| = |.g1.| by A2, PARTFUN1:5; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let W be non empty set ; ::_thesis: 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
let f1, f2 be PartFunc of W,(REAL-NS n); ::_thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let g1, g2 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2
A2: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2;
then A3: dom (f1 - f2) = dom (g1 - g2) by A1, VALUED_2:def_46;
A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_._x_=_(g1_-_g2)_._x
let x be Element of W; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (g1 - g2) . x )
assume A5: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (g1 - g2) . x
A6: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def_4;
( x in dom f1 & x in dom f2 ) by A5, A2, XBOOLE_0:def_4;
then ( g1 . x = g1 /. x & g2 /. x = g2 . x ) by A1, PARTFUN1:def_6;
then A7: (f1 /. x) - (f2 /. x) = (g1 . x) - (g2 . x) by A6, REAL_NS1:5;
A8: (f1 - f2) /. x = (f1 /. x) - (f2 /. x) by A5, VFUNCT_1:def_2;
(f1 - f2) /. x = (f1 - f2) . x by A5, PARTFUN1:def_6;
hence (f1 - f2) . x = (g1 - g2) . x by A7, A8, A3, A5, VALUED_2:def_46; ::_thesis: verum
end;
f1 - f2 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence f1 - f2 = g1 - g2 by A3, A4, PARTFUN1:5; ::_thesis: verum
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 ) ) )
proof
let n be Element of NAT ; ::_thesis: 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 ) ) )
let x0 be real number ; ::_thesis: 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 ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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 ) ) )
thus ( f is_continuous_in x0 implies ( 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 ) ) ) ::_thesis: ( 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 ) implies f is_continuous_in x0 )
proof
assume f is_continuous_in x0 ; ::_thesis: ( 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 ) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_continuous_in x0 ) by Def1;
thus x0 in dom f by A1, NFCONT_3:9; ::_thesis: 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
let N01 be Subset of (REAL n); ::_thesis: ( ex r being Real st
( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) implies ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01 )
assume A2: ex r being Real st
( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) ; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01
consider r being Real such that
A3: 0 < r and
A4: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = N01 by A2;
f /. x0 = g /. x0 by A1, REAL_NS1:def_4;
then A5: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } = N01 by A4, Th4;
{ p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } is Neighbourhood of g /. x0 by A3, NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A6: for x1 being real number st x1 in dom g & x1 in N holds
g /. x1 in N01 by A5, A1, NFCONT_3:9;
take N ; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01
let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N01 )
assume ( x1 in dom f & x1 in N ) ; ::_thesis: f /. x1 in N01
then g /. x1 in N01 by A1, A6;
hence f /. x1 in N01 by A1, REAL_NS1:def_4; ::_thesis: verum
end;
assume A7: ( 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 ) ) ; ::_thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_N1_being_Neighbourhood_of_g_/._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x1_being_real_number_st_x1_in_dom_g_&_x1_in_N_holds_
g_/._x1_in_N1
let N1 be Neighbourhood of g /. x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom g & x1 in N holds
g /. x1 in N1
consider r being Real such that
A8: 0 < r and
A9: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def_1;
set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ;
f /. x0 = g /. x0 by REAL_NS1:def_4;
then A10: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;
now__::_thesis:_for_x_being_set_st_x_in__{__p_where_p_is_Element_of_REAL_n_:_|.(p_-_(f_/._x0)).|_<_r__}__holds_
x_in_REAL_n
let x be set ; ::_thesis: ( x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } implies x in REAL n )
assume x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; ::_thesis: x in REAL n
then ex p being Element of REAL n st
( p = x & |.(p - (f /. x0)).| < r ) ;
hence x in REAL n ; ::_thesis: verum
end;
then { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } is Subset of (REAL n) by TARSKI:def_3;
then consider N being Neighbourhood of x0 such that
A11: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A7, A8;
take N = N; ::_thesis: for x1 being real number st x1 in dom g & x1 in N holds
g /. x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom g & x1 in N implies g /. x1 in N1 )
assume ( x1 in dom g & x1 in N ) ; ::_thesis: g /. x1 in N1
then f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A11;
then g /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by REAL_NS1:def_4;
hence g /. x1 in N1 by A9, A10; ::_thesis: verum
end;
then g is_continuous_in x0 by A7, NFCONT_3:9;
hence f is_continuous_in x0 by Def1; ::_thesis: verum
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 ) ) )
proof
let n be Element of NAT ; ::_thesis: 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 ) ) )
let x0 be real number ; ::_thesis: 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 ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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 ) ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
hereby ::_thesis: ( 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 ) implies f is_continuous_in x0 )
assume f is_continuous_in x0 ; ::_thesis: ( 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 ) )
then A1: g is_continuous_in x0 by Th1;
hence x0 in dom f by NFCONT_3:10; ::_thesis: 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
thus 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 ::_thesis: verum
proof
let N1 be Subset of (REAL n); ::_thesis: ( ex r being Real st
( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) implies ex N being Neighbourhood of x0 st f .: N c= N1 )
given r being Real such that A2: ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) ; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1
f /. x0 = g /. x0 by REAL_NS1:def_4;
then A3: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;
N1 is Neighbourhood of g /. x0 by A2, A3, NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A4: g .: N c= N1 by A1, NFCONT_3:10;
take N ; ::_thesis: f .: N c= N1
thus f .: N c= N1 by A4; ::_thesis: verum
end;
end;
assume A5: ( 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 ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_N1_being_Neighbourhood_of_g_/._x0_ex_N_being_Neighbourhood_of_x0_st_g_.:_N_c=_N1
let N1 be Neighbourhood of g /. x0; ::_thesis: ex N being Neighbourhood of x0 st g .: N c= N1
consider r being Real such that
A6: 0 < r and
A7: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def_1;
set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ;
f /. x0 = g /. x0 by REAL_NS1:def_4;
then A8: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;
now__::_thesis:_for_x_being_set_st_x_in__{__p_where_p_is_Element_of_REAL_n_:_|.(p_-_(f_/._x0)).|_<_r__}__holds_
x_in_REAL_n
let x be set ; ::_thesis: ( x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } implies x in REAL n )
assume x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; ::_thesis: x in REAL n
then ex p being Element of REAL n st
( p = x & |.(p - (f /. x0)).| < r ) ;
hence x in REAL n ; ::_thesis: verum
end;
then { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } is Subset of (REAL n) by TARSKI:def_3;
then consider N being Neighbourhood of x0 such that
A9: f .: N c= { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A5, A6;
take N = N; ::_thesis: g .: N c= N1
thus g .: N c= N1 by A7, A8, A9, XBOOLE_1:1; ::_thesis: verum
end;
then g is_continuous_in x0 by A5, NFCONT_3:10;
hence f is_continuous_in x0 by Th1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: 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
let f be PartFunc of REAL,(REAL n); ::_thesis: ( ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 )
given N being Neighbourhood of x0 such that A1: (dom f) /\ N = {x0} ; ::_thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is_continuous_in x0 by A1, NFCONT_3:11;
hence f is_continuous_in x0 by Th1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: 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
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1 + f2 is_continuous_in x0 )
assume A1: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: f1 + f2 is_continuous_in x0
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
g2 is_continuous_in x0 by A1, Th1;
then A3: ( g1 + g2 is_continuous_in x0 & g1 - g2 is_continuous_in x0 ) by A1, A2, NFCONT_3:12;
g1 + g2 = f1 + f2 by Th5;
hence f1 + f2 is_continuous_in x0 by A3, Th1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: 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
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1 - f2 is_continuous_in x0 )
assume A1: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: f1 - f2 is_continuous_in x0
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
g2 is_continuous_in x0 by A1, Th1;
then A3: ( g1 + g2 is_continuous_in x0 & g1 - g2 is_continuous_in x0 ) by A1, A2, NFCONT_3:12;
g1 - g2 = f1 - f2 by Th10;
hence f1 - f2 is_continuous_in x0 by A3, Th1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let r be Real; ::_thesis: 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
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; ::_thesis: r (#) f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is_continuous_in x0 by A1, Th1;
then A2: r (#) g is_continuous_in x0 by NFCONT_3:13;
r (#) g = r (#) f by Th6;
hence r (#) f is_continuous_in x0 by A2, Th1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies |.f.| is_continuous_in x0 )
assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; ::_thesis: |.f.| is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is_continuous_in x0 by A1, Th1;
then ||.g.|| is_continuous_in x0 by A1, NFCONT_3:14;
hence |.f.| is_continuous_in x0 by Th9; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
- f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies - f is_continuous_in x0 )
assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; ::_thesis: - f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is_continuous_in x0 by A1, Th1;
then A2: - g is_continuous_in x0 by A1, NFCONT_3:14;
- g = - f by Th8;
hence - f is_continuous_in x0 by A2, Th1; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let z be Point of (REAL-NS n); ::_thesis: 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
let f1 be PartFunc of REAL,(REAL n); ::_thesis: 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
let f2 be PartFunc of (REAL-NS n),S; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z implies f2 * f1 is_continuous_in x0 )
assume A1: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z ) ; ::_thesis: f2 * f1 is_continuous_in x0
reconsider g1 = f1 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
f1 /. x0 = g1 /. x0 by REAL_NS1:def_4;
hence f2 * f1 is_continuous_in x0 by A2, A1, NFCONT_3:15; ::_thesis: verum
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
proof
let x0 be real number ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f1 be PartFunc of REAL,S; ::_thesis: 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
let f2 be PartFunc of S,REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0 ; ::_thesis: f2 * f1 is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) )
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) )
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
A7: rng (f1 /* s1) c= dom f2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f1 /* s1) or x in dom f2 )
assume x in rng (f1 /* s1) ; ::_thesis: x in dom f2
then consider n being Element of NAT such that
A8: x = (f1 /* s1) . n by FUNCT_2:113;
s1 . n in rng s1 by VALUED_0:28;
then f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11;
hence x in dom f2 by A4, A6, A8, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum
end;
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n
let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
s1 . n in rng s1 by VALUED_0:28;
then A10: s1 . n in dom f1 by A4, FUNCT_1:11;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by A7, FUNCT_2:108 ; ::_thesis: verum
end;
then A11: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
rng s1 c= dom f1 by A4, A6, XBOOLE_1:1;
then A12: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, NFCONT_3:def_1;
hence (f2 * f1) /* s1 is convergent by A3, A7, A11, NFCONT_1:def_6; ::_thesis: (f2 * f1) . x0 = lim ((f2 * f1) /* s1)
thus (f2 * f1) . x0 = (f2 * f1) /. x0 by A1, PARTFUN1:def_6
.= f2 /. (f1 /. x0) by A1, PARTFUN2:3
.= lim (f2 /* (f1 /* s1)) by A12, A3, A7, NFCONT_1:def_6
.= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x0 be Element of REAL n;
predf 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 );
end;
:: 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 ) );
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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let f be PartFunc of (REAL n),REAL; ::_thesis: 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 )
let h be PartFunc of (REAL-NS n),REAL; ::_thesis: 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 )
let x0 be Element of REAL n; ::_thesis: 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 )
let y0 be Point of (REAL-NS n); ::_thesis: ( f = h & x0 = y0 implies ( f is_continuous_in x0 iff h is_continuous_in y0 ) )
assume A1: ( f = h & x0 = y0 ) ; ::_thesis: ( f is_continuous_in x0 iff h is_continuous_in y0 )
hereby ::_thesis: ( h is_continuous_in y0 implies f is_continuous_in x0 )
assume f is_continuous_in x0 ; ::_thesis: h is_continuous_in y0
then ex y1 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y1 & f = g & g is_continuous_in y1 ) by Def4;
hence h is_continuous_in y0 by A1; ::_thesis: verum
end;
thus ( h is_continuous_in y0 implies f is_continuous_in x0 ) by A1, Def4; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let x0 be real number ; ::_thesis: 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
let f1 be PartFunc of REAL,(REAL n); ::_thesis: 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
let f2 be PartFunc of (REAL n),REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 ) ; ::_thesis: f2 * f1 is_continuous_in x0
reconsider g1 = f1 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
reconsider g2 = f2 as PartFunc of (REAL-NS n),REAL by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
f1 /. x0 = g1 /. x0 by REAL_NS1:def_4;
then g2 is_continuous_in g1 /. x0 by A1, Th21;
hence f2 * f1 is_continuous_in x0 by A2, A1, Th20; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is continuous means :Def5: :: NFCONT_4:def 5
for x0 being real number st x0 in dom f holds
f is_continuous_in x0;
end;
:: 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 );
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
let n be Element of NAT ; ::_thesis: 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 )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( g = f implies ( g is continuous iff f is continuous ) )
assume A1: g = f ; ::_thesis: ( g is continuous iff f is continuous )
hereby ::_thesis: ( f is continuous implies g is continuous )
assume A2: g is continuous ; ::_thesis: f is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_f_holds_
f_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom f implies f is_continuous_in x0 )
assume x0 in dom f ; ::_thesis: f is_continuous_in x0
then g is_continuous_in x0 by A2, A1, NFCONT_3:def_2;
hence f is_continuous_in x0 by A1, Th1; ::_thesis: verum
end;
hence f is continuous by Def5; ::_thesis: verum
end;
assume A3: f is continuous ; ::_thesis: g is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_g_holds_
g_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom g implies g is_continuous_in x0 )
assume x0 in dom g ; ::_thesis: g is_continuous_in x0
then f is_continuous_in x0 by A3, A1, Def5;
hence g is_continuous_in x0 by A1, Th1; ::_thesis: verum
end;
hence g is continuous by NFCONT_3:def_2; ::_thesis: verum
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 ) ) )
proof
let n be Element of NAT ; ::_thesis: 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 ) ) )
let X be set ; ::_thesis: 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 ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f implies ( 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 ) ) ) )
assume A1: X c= dom f ; ::_thesis: ( 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 ) ) )
thus ( f | X is continuous implies 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 ) ) ) ::_thesis: ( ( 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 ) ) ) implies f | X is continuous )
proof
assume A2: f | X is continuous ; ::_thesis: 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 ) )
let x0 be real number ; ::_thesis: 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 ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies 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 ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: 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 ) )
x0 in dom (f | X) by A1, A3, RELAT_1:62;
then f | X is_continuous_in x0 by A2, Def5;
then consider s being real number such that
A5: 0 < s and
A6: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th3;
take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s by A5; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume that
A7: x1 in X and
A8: abs (x1 - x0) < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
A9: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2:15
.= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2:15 ;
hence |.((f /. x1) - (f /. x0)).| < r by A6, A9, A7, A8; ::_thesis: verum
end;
assume A10: 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 ) ) ; ::_thesis: f | X is continuous
A11: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A12: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
A13: x0 in X by A12, RELAT_1:57;
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 | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) )
assume 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
then consider s being real number such that
A14: 0 < s and
A15: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r by A10, A13;
take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
thus 0 < s by A14; ::_thesis: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in dom (f | X) & abs (x1 - x0) < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < r )
assume that
A16: x1 in dom (f | X) and
A17: abs (x1 - x0) < s ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < r
|.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, PARTFUN2:15
.= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2:15 ;
hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A11, A15, A16, A17; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by Th3, A12; ::_thesis: verum
end;
hence f | X is continuous by Def5; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster Function-like constant -> continuous for Element of bool [:REAL,(REAL n):];
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds
b1 is continuous
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is constant implies f is continuous )
assume A1: f is constant ; ::_thesis: f is continuous
now__::_thesis:_for_x0_being_real_number_
for_r_being_Real_st_x0_in_dom_f_&_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_)_)
reconsider s = 1 as real number ;
let x0 be real number ; ::_thesis: for r being Real st x0 in dom f & 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 ) )
let r be Real; ::_thesis: ( x0 in dom f & 0 < r implies 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 ) ) )
assume that
A2: x0 in dom f and
A3: 0 < r ; ::_thesis: 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 ) )
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s ; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume A4: x1 in dom f ; ::_thesis: ( abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume abs (x1 - x0) < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
f /. x1 = f . x1 by A4, PARTFUN1:def_6
.= f . x0 by A1, A2, A4, FUNCT_1:def_10
.= f /. x0 by A2, PARTFUN1:def_6 ;
hence |.((f /. x1) - (f /. x0)).| < r by A3; ::_thesis: verum
end;
then f | (dom f) is continuous by Th24;
hence f is continuous by RELAT_1:69; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
cluster Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() continuous for Element of bool [:REAL,(REAL n):];
existence
ex b1 being PartFunc of REAL,(REAL n) st b1 is continuous
proof
take f = the constant PartFunc of REAL,(REAL n); ::_thesis: f is continuous
thus f is continuous ; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let X be set ;
clusterf | X -> continuous for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous
proof
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A1: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in dom f by RELAT_1:57;
then A2: f is_continuous_in x0 by Def5;
x0 in X by A1, RELAT_1:57;
hence f | X is_continuous_in x0 by A2, Th2; ::_thesis: verum
end;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous by Def5; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds
f | X1 is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous )
assume A1: f | X is continuous ; ::_thesis: ( not X1 c= X or f | X1 is continuous )
assume X1 c= X ; ::_thesis: f | X1 is continuous
then f | X1 = (f | X) | X1 by RELAT_1:74;
hence f | X1 is continuous by A1; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster empty Function-like -> continuous for Element of bool [:REAL,(REAL n):];
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds
b1 is continuous ;
end;
registration
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let X be trivial set ;
clusterf | X -> continuous for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | X is continuous PartFunc of REAL,(REAL-NS n) ;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous by Th23; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
let f1, f2 be continuous PartFunc of REAL,(REAL n);
clusterf1 + f2 -> continuous for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is continuous
proof
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: ( g1 is continuous & g2 is continuous ) by Th23;
g1 + g2 = f1 + f2 by Th5;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is continuous by A1, Th23; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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 )
let X be set ; ::_thesis: 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 )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) )
assume A1: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous ) ; ::_thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 | X is continuous by A1, Th23;
g2 | X is continuous by A1, Th23;
then A3: ( (g1 + g2) | X is continuous & (g1 - g2) | X is continuous ) by A1, A2, NFCONT_3:19;
A4: g1 + g2 = f1 + f2 by Th5;
g1 - g2 = f1 - f2 by Th10;
hence ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) by A3, A4, Th23; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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 )
let X, X1 be set ; ::_thesis: 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 )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous implies ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) )
assume A1: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous ) ; ::_thesis: ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 | X is continuous by A1, Th23;
g2 | X1 is continuous by A1, Th23;
then A3: ( (g1 + g2) | (X /\ X1) is continuous & (g1 - g2) | (X /\ X1) is continuous ) by A1, A2, NFCONT_3:20;
A4: g1 + g2 = f1 + f2 by Th5;
g1 - g2 = f1 - f2 by Th10;
hence ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) by A3, A4, Th23; ::_thesis: verum
end;
registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let r be Real;
clusterr (#) f -> continuous for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds
b1 is continuous
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: g is continuous by Th23;
r (#) g = r (#) f by Th6;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds
b1 is continuous by A1, Th23; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let X be set ; ::_thesis: 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
let r be Real; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume A1: ( X c= dom f & f | X is continuous ) ; ::_thesis: (r (#) f) | X is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | X is continuous PartFunc of REAL,(REAL-NS n) by A1, Th23;
then A2: (r (#) g) | X is continuous by A1, NFCONT_3:21;
r (#) g = r (#) f by Th6;
hence (r (#) f) | X is continuous by A2, Th23; ::_thesis: verum
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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let X be set ; ::_thesis: 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 )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f & f | X is continuous implies ( |.f.| | X is continuous & (- f) | X is continuous ) )
assume A1: ( X c= dom f & f | X is continuous ) ; ::_thesis: ( |.f.| | X is continuous & (- f) | X is continuous )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | X is continuous by A1, Th23;
then A2: ( ||.g.|| | X is continuous & (- g) | X is continuous ) by A1, NFCONT_3:22;
hence |.f.| | X is continuous by Th9; ::_thesis: (- f) | X is continuous
- g = - f by Th8;
hence (- f) | X is continuous by A2, Th23; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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 implies f | REAL is continuous )
assume A1: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) ) ; ::_thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous )
given x0 being real number such that A2: f is_continuous_in x0 ; ::_thesis: f | REAL is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: now__::_thesis:_for_x1,_x2_being_real_number_holds_g_/._(x1_+_x2)_=_(g_/._x1)_+_(g_/._x2)
let x1, x2 be real number ; ::_thesis: g /. (x1 + x2) = (g /. x1) + (g /. x2)
A4: ( g /. x1 = f /. x1 & g /. x2 = f /. x2 ) by REAL_NS1:def_4;
thus g /. (x1 + x2) = f /. (x1 + x2) by REAL_NS1:def_4
.= (f /. x1) + (f /. x2) by A1
.= (g /. x1) + (g /. x2) by A4, REAL_NS1:2 ; ::_thesis: verum
end;
g is_continuous_in x0 by A2, Th1;
then g | REAL is continuous by A1, A3, NFCONT_3:23;
hence f | REAL is continuous by Th23; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let f be PartFunc of REAL,(REAL n); ::_thesis: 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
let Y be Subset of (REAL-NS n); ::_thesis: ( dom f is compact & f | (dom f) is continuous & Y = rng f implies Y is compact )
assume A1: ( dom f is compact & f | (dom f) is continuous & Y = rng f ) ; ::_thesis: Y is compact
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | (dom g) is continuous by A1, Th23;
hence Y is compact by A1, NFCONT_3:24; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let f be PartFunc of REAL,(REAL n); ::_thesis: 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
let Y be Subset of REAL; ::_thesis: 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
let Z be Subset of (REAL-NS n); ::_thesis: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous implies Z is compact )
assume A1: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous ) ; ::_thesis: Z is compact
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | Y is continuous by A1, Th23;
hence Z is compact by A1, NFCONT_3:25; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is Lipschitzian means :Def6: :: NFCONT_4:def 6
ex g being PartFunc of REAL,(REAL-NS n) st
( g = f & g is Lipschitzian );
end;
:: 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 ) );
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)) ) ) )
proof
let n be Element of NAT ; ::_thesis: 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)) ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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)) ) ) )
hereby ::_thesis: ( 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)) ) ) implies f is Lipschitzian )
assume f is Lipschitzian ; ::_thesis: 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)) ) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( g = f & g is Lipschitzian ) by Def6;
consider r being real number such that
A2: ( 0 < r & ( for x1, x2 being real number st x1 in dom g & x2 in dom g holds
||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) ) ) by A1, NFCONT_3:def_3;
take r = r; ::_thesis: ( 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)) ) )
thus 0 < r by A2; ::_thesis: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
thus for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ::_thesis: verum
proof
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume ( x1 in dom f & x2 in dom f ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then A3: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A1, A2;
( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by A1, REAL_NS1:def_4;
hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
end;
given r being real number such that A4: ( 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)) ) ) ; ::_thesis: f is Lipschitzian
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_g_&_x2_in_dom_g_holds_
||.((g_/._x1)_-_(g_/._x2)).||_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom g & x2 in dom g implies ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) )
assume ( x1 in dom g & x2 in dom g ) ; ::_thesis: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2))
then A5: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4;
( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by REAL_NS1:def_4;
hence ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A5, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
then g is Lipschitzian by A4, NFCONT_3:def_3;
hence f is Lipschitzian by Def6; ::_thesis: verum
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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = h implies ( f is Lipschitzian iff h is Lipschitzian ) )
assume A1: f = h ; ::_thesis: ( f is Lipschitzian iff h is Lipschitzian )
hereby ::_thesis: ( h is Lipschitzian implies f is Lipschitzian )
assume f is Lipschitzian ; ::_thesis: h is Lipschitzian
then consider r being real number such that
A2: ( 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)) ) ) by Th33;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_h_&_x2_in_dom_h_holds_
||.((h_/._x1)_-_(h_/._x2)).||_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom h & x2 in dom h implies ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) )
assume ( x1 in dom h & x2 in dom h ) ; ::_thesis: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2))
then A3: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A2, A1;
( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by A1, REAL_NS1:def_4;
hence ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
hence h is Lipschitzian by A2, NFCONT_3:def_3; ::_thesis: verum
end;
assume h is Lipschitzian ; ::_thesis: f is Lipschitzian
then consider r being real number such that
A4: ( 0 < r & ( for x1, x2 being real number st x1 in dom h & x2 in dom h holds
||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) ) ) by NFCONT_3:def_3;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
|.((f_/._x1)_-_(f_/._x2)).|_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume ( x1 in dom f & x2 in dom f ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then A5: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A4, A1;
( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by A1, REAL_NS1:def_4;
hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A5, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
hence f is Lipschitzian by A4, Th33; ::_thesis: verum
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)) ) ) )
proof
let n be Element of NAT ; ::_thesis: 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)) ) ) )
let X be set ; ::_thesis: 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)) ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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)) ) ) )
hereby ::_thesis: ( 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)) ) ) implies f | X is Lipschitzian )
assume f | X is Lipschitzian ; ::_thesis: 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)) ) )
then consider r being real number such that
A1: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) ) ) by Th33;
take r = r; ::_thesis: ( 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)) ) )
thus 0 < r by A1; ::_thesis: 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))
thus 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)) ::_thesis: verum
proof
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume A2: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A1;
then |.((f /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A2, PARTFUN2:15;
hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A2, PARTFUN2:15; ::_thesis: verum
end;
end;
given r being real number such that A3: ( 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)) ) ) ; ::_thesis: f | X is Lipschitzian
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_
|.(((f_|_X)_/._x1)_-_((f_|_X)_/._x2)).|_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) )
assume A4: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2))
then |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A3;
then |.(((f | X) /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4, PARTFUN2:15;
hence |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A4, PARTFUN2:15; ::_thesis: verum
end;
hence f | X is Lipschitzian by A3, Th33; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster empty Function-like -> Lipschitzian for Element of bool [:REAL,(REAL n):];
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is empty implies f is Lipschitzian )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
assume f is empty ; ::_thesis: f is Lipschitzian
then g is empty ;
hence f is Lipschitzian by Th34; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
cluster empty Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() for Element of bool [:REAL,(REAL n):];
existence
ex b1 being PartFunc of REAL,(REAL n) st b1 is empty
proof
take the empty PartFunc of REAL,(REAL n) ; ::_thesis: the empty PartFunc of REAL,(REAL n) is empty
thus the empty PartFunc of REAL,(REAL n) is empty ; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let X be set ;
clusterf | X -> Lipschitzian for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is Lipschitzian
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is Lipschitzian by Th34;
then g | X is Lipschitzian ;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is Lipschitzian by Th34; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian & X1 c= X implies f | X1 is Lipschitzian )
assume that
A1: f | X is Lipschitzian and
A2: X1 c= X ; ::_thesis: f | X1 is Lipschitzian
f | X1 = (f | X) | X1 by A2, RELAT_1:74;
hence f | X1 is Lipschitzian by A1; ::_thesis: verum
end;
registration
let n be Element of NAT ;
let f1, f2 be Lipschitzian PartFunc of REAL,(REAL n);
clusterf1 + f2 -> Lipschitzian for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is Lipschitzian
proof
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Th34;
g1 + g2 = f1 + f2 by Th5;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is Lipschitzian by A1, Th34; ::_thesis: verum
end;
clusterf1 - f2 -> Lipschitzian for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds
b1 is Lipschitzian
proof
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Th34;
g1 - g2 = f1 - f2 by Th10;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds
b1 is Lipschitzian by A2, Th34; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let X, X1 be set ; ::_thesis: 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
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian )
assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 + f2) | (X /\ X1) is Lipschitzian
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by Th34, A1;
then A2: (g1 + g2) | (X /\ X1) is Lipschitzian by NFCONT_3:28;
g1 + g2 = f1 + f2 by Th5;
hence (f1 + f2) | (X /\ X1) is Lipschitzian by A2, Th34; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let X, X1 be set ; ::_thesis: 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
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 - f2) | (X /\ X1) is Lipschitzian )
assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 - f2) | (X /\ X1) is Lipschitzian
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by Th34, A1;
then A2: (g1 - g2) | (X /\ X1) is Lipschitzian by NFCONT_3:29;
g1 - g2 = f1 - f2 by Th10;
hence (f1 - f2) | (X /\ X1) is Lipschitzian by A2, Th34; ::_thesis: verum
end;
registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let p be Real;
clusterp (#) f -> Lipschitzian for PartFunc of REAL,(REAL n);
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 = p (#) f holds
b1 is Lipschitzian
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: g is Lipschitzian by Th34;
p (#) g = p (#) f by Th6;
hence for b1 being PartFunc of REAL,(REAL n) st b1 = p (#) f holds
b1 is Lipschitzian by A1, Th34; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let X be set ; ::_thesis: 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
let p be Real; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )
assume A1: ( f | X is Lipschitzian & X c= dom f ) ; ::_thesis: (p (#) f) | X is Lipschitzian
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | X is Lipschitzian by Th34, A1;
then A2: (p (#) g) | X is Lipschitzian by A1, NFCONT_3:30;
p (#) g = p (#) f by Th6;
hence (p (#) f) | X is Lipschitzian by A2, Th34; ::_thesis: verum
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
for b1 being PartFunc of REAL,REAL st b1 = |.f.| holds
b1 is Lipschitzian
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is Lipschitzian by Th34;
then ||.g.|| is Lipschitzian ;
hence for b1 being PartFunc of REAL,REAL st b1 = |.f.| holds
b1 is Lipschitzian by Th9; ::_thesis: verum
end;
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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let X be set ; ::_thesis: 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 )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) )
assume A1: f | X is Lipschitzian ; ::_thesis: ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g | X is Lipschitzian by A1, Th34;
then A2: ( - (g | X) is Lipschitzian & ||.g.|| | X is Lipschitzian & (- g) | X is Lipschitzian ) by NFCONT_3:31;
- (g | X) = - (f | X) by Th8;
hence - (f | X) is Lipschitzian by A2, Th34; ::_thesis: ( |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
thus |.f.| | X is Lipschitzian by A2, Th9; ::_thesis: (- f) | X is Lipschitzian
- g = - f by Th8;
hence (- f) | X is Lipschitzian by A2, Th34; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster Function-like constant -> Lipschitzian for Element of bool [:REAL,(REAL n):];
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is constant implies f is Lipschitzian )
assume A1: f is constant ; ::_thesis: f is Lipschitzian
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
g is constant by A1;
hence f is Lipschitzian by Th34; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
cluster Function-like Lipschitzian -> continuous for Element of bool [:REAL,(REAL n):];
coherence
for b1 being PartFunc of REAL,(REAL n) st b1 is Lipschitzian holds
b1 is continuous
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is Lipschitzian implies f is continuous )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
assume f is Lipschitzian ; ::_thesis: f is continuous
then g is Lipschitzian by Th34;
hence f is continuous by Th23; ::_thesis: verum
end;
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
proof
let n be Element of NAT ; ::_thesis: 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
let X be set ; ::_thesis: 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
let f be PartFunc of REAL,(REAL n); ::_thesis: 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
let r, p be Element of REAL n; ::_thesis: ( ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) implies f | X is continuous )
assume A1: for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ; ::_thesis: f | X is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
reconsider r0 = r, p0 = p as Point of (REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_x0_being_real_number_st_x0_in_X_holds_
g_/._x0_=_(x0_*_r0)_+_p0
let x0 be real number ; ::_thesis: ( x0 in X implies g /. x0 = (x0 * r0) + p0 )
assume A2: x0 in X ; ::_thesis: g /. x0 = (x0 * r0) + p0
A3: x0 * r = x0 * r0 by REAL_NS1:3;
thus g /. x0 = f /. x0 by REAL_NS1:def_4
.= (x0 * r) + p by A2, A1
.= (x0 * r0) + p0 by A3, REAL_NS1:2 ; ::_thesis: verum
end;
then g | X is continuous by NFCONT_3:33;
hence f | X is continuous by Th23; ::_thesis: verum
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
let n, i be Element of NAT ; ::_thesis: for x0 being Element of REAL n st 1 <= i & i <= n holds
proj (i,n) is_continuous_in x0
let x0 be Element of REAL n; ::_thesis: ( 1 <= i & i <= n implies proj (i,n) is_continuous_in x0 )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: proj (i,n) is_continuous_in x0
A2: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
reconsider prg = proj (i,n) as PartFunc of (REAL-NS n),REAL by REAL_NS1:def_4;
reconsider px0 = x0 as Element of (REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_px1_being_Element_of_(REAL-NS_n)_st_px1_in_dom_prg_&_||.(px1_-_px0).||_<_s_holds_
|.(((proj_(i,n))_/._px1)_-_((proj_(i,n))_/._px0)).|_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) ) )
assume A3: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )
take s = r; ::_thesis: ( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )
thus 0 < s by A3; ::_thesis: for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r
now__::_thesis:_for_px1_being_Element_of_(REAL-NS_n)_st_px1_in_dom_prg_&_||.(px1_-_px0).||_<_r_holds_
|.(((proj_(i,n))_/._px1)_-_((proj_(i,n))_/._px0)).|_<_r
let px1 be Element of (REAL-NS n); ::_thesis: ( px1 in dom prg & ||.(px1 - px0).|| < r implies |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r )
assume A4: ( px1 in dom prg & ||.(px1 - px0).|| < r ) ; ::_thesis: |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r
reconsider x1 = px1 as Element of REAL n by REAL_NS1:def_4;
A5: ||.(px1 - px0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
(proj (i,n)) /. (x1 - x0) = ((proj (i,n)) /. x1) - ((proj (i,n)) /. x0) by A1, PDIFF_8:12;
then |.(((proj (i,n)) /. x1) - ((proj (i,n)) /. x0)).| <= |.(x1 - x0).| by A1, PDIFF_8:5;
hence |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r by A4, A5, XXREAL_0:2; ::_thesis: verum
end;
hence for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ; ::_thesis: verum
end;
then prg is_continuous_in px0 by A2, NFCONT_1:8;
hence proj (i,n) is_continuous_in x0 by Def4; ::_thesis: verum
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 ) ) )
proof
let x0 be real number ; ::_thesis: 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 ) ) )
let n be non empty Element of NAT ; ::_thesis: 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 ) ) )
let h be PartFunc of REAL,(REAL n); ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 )
assume A1: h is_continuous_in x0 ; ::_thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) )
hence A2: x0 in dom h by Th3; ::_thesis: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0
thus for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume i in Seg n ; ::_thesis: (proj (i,n)) * h is_continuous_in x0
then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A4: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
rng h c= REAL n ;
then A5: dom ((proj (i,n)) * h) = dom h by A4, RELAT_1:27;
proj (i,n) is_continuous_in h /. x0 by A3, Th42;
hence (proj (i,n)) * h is_continuous_in x0 by A5, A1, A2, Th22; ::_thesis: verum
end;
end;
assume A6: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) ; ::_thesis: h is_continuous_in x0
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 h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r ) )
proof
let r0 be Real; ::_thesis: ( 0 < r0 implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) ) )
assume A7: 0 < r0 ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
set r = r0 / 2;
A8: 0 < r0 / 2 by A7, XREAL_1:215;
defpred S1[ Nat, real number ] means ( 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
|.((((proj ($1,n)) * h) . x1) - (((proj ($1,n)) * h) . x0)).| < (r0 / 2) / n ) );
A9: 0 < (r0 / 2) / n by A8, XREAL_1:139;
A10: for j being Nat st j in Seg n holds
ex x being Element of REAL st S1[j,x]
proof
let j be Nat; ::_thesis: ( j in Seg n implies ex x being Element of REAL st S1[j,x] )
assume A11: j in Seg n ; ::_thesis: ex x being Element of REAL st S1[j,x]
A12: (proj (j,n)) * h is_continuous_in x0 by A6, A11;
A13: dom (proj (j,n)) = REAL n by FUNCT_2:def_1;
rng h c= REAL n ;
then A14: dom ((proj (j,n)) * h) = dom h by A13, RELAT_1:27;
consider sj being real number such that
A15: ( 0 < sj & ( for x1 being real number st x1 in dom ((proj (j,n)) * h) & abs (x1 - x0) < sj holds
|.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n ) ) by A12, A9, FCONT_1:3;
sj is Real by XREAL_0:def_1;
hence ex x being Element of REAL st S1[j,x] by A15, A14; ::_thesis: verum
end;
consider s0 being FinSequence of REAL such that
A16: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A10);
n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A16, FUNCT_1:3;
rng s0 is finite by A16, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
A17: min rs0 in rng s0 by XXREAL_2:def_7;
then reconsider s = min rs0 as Real ;
take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
ex i1 being set st
( i1 in dom s0 & s = s0 . i1 ) by A17, FUNCT_1:def_3;
hence 0 < s by A16; ::_thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0
now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_h_&_abs_(x1_-_x0)_<_s_holds_
|.((h_/._x1)_-_(h_/._x0)).|_<_r0
let x1 be real number ; ::_thesis: ( x1 in dom h & abs (x1 - x0) < s implies |.((h /. x1) - (h /. x0)).| < r0 )
assume A18: ( x1 in dom h & abs (x1 - x0) < s ) ; ::_thesis: |.((h /. x1) - (h /. x0)).| < r0
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
|.((proj_(j,n))_._((h_/._x1)_-_(h_/._x0))).|_<=_(r0_/_2)_/_n
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n )
assume ( 1 <= j & j <= n ) ; ::_thesis: |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n
then A19: j in Seg n by FINSEQ_1:1;
then s0 . j in rng s0 by A16, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def_7;
then abs (x1 - x0) < s0 . j by A18, XXREAL_0:2;
then A20: |.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n by A19, A18, A16;
A21: ((proj (j,n)) * h) . x1 = (proj (j,n)) . (h . x1) by A18, FUNCT_1:13
.= (proj (j,n)) . (h /. x1) by A18, PARTFUN1:def_6 ;
((proj (j,n)) * h) . x0 = (proj (j,n)) . (h . x0) by A6, FUNCT_1:13
.= (proj (j,n)) . (h /. x0) by A6, PARTFUN1:def_6 ;
hence |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n by A20, A21, PDIFF_8:12; ::_thesis: verum
end;
then |.((h /. x1) - (h /. x0)).| <= n * ((r0 / 2) / n) by PDIFF_8:17;
then A22: |.((h /. x1) - (h /. x0)).| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A7, XREAL_1:216;
hence |.((h /. x1) - (h /. x0)).| < r0 by A22, XXREAL_0:2; ::_thesis: verum
end;
hence for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ; ::_thesis: verum
end;
hence h is_continuous_in x0 by A6, Th3; ::_thesis: verum
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 )
proof
let n be non empty Element of NAT ; ::_thesis: 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 )
let h be PartFunc of REAL,(REAL n); ::_thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous )
hereby ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous ) implies h is continuous )
assume A1: h is continuous ; ::_thesis: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous
thus for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is continuous )
assume A2: i in Seg n ; ::_thesis: (proj (i,n)) * h is continuous
A3: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
rng h c= REAL n ;
then A4: dom ((proj (i,n)) * h) = dom h by A3, RELAT_1:27;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_((proj_(i,n))_*_h)_holds_
(proj_(i,n))_*_h_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom ((proj (i,n)) * h) implies (proj (i,n)) * h is_continuous_in x0 )
assume x0 in dom ((proj (i,n)) * h) ; ::_thesis: (proj (i,n)) * h is_continuous_in x0
then h is_continuous_in x0 by A1, A4, Def5;
hence (proj (i,n)) * h is_continuous_in x0 by A2, Th43; ::_thesis: verum
end;
hence (proj (i,n)) * h is continuous by FCONT_1:def_2; ::_thesis: verum
end;
end;
assume A5: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous ; ::_thesis: h is continuous
let x0 be real number ; :: according to NFCONT_4:def_5 ::_thesis: ( x0 in dom h implies h is_continuous_in x0 )
assume A6: x0 in dom h ; ::_thesis: h is_continuous_in x0
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(proj_(i,n))_*_h_is_continuous_in_x0
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume A7: i in Seg n ; ::_thesis: (proj (i,n)) * h is_continuous_in x0
A8: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
rng h c= REAL n ;
then A9: dom ((proj (i,n)) * h) = dom h by A8, RELAT_1:27;
(proj (i,n)) * h is continuous by A5, A7;
hence (proj (i,n)) * h is_continuous_in x0 by A6, A9, FCONT_1:def_2; ::_thesis: verum
end;
hence h is_continuous_in x0 by A6, Th43; ::_thesis: verum
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
let n, i be Element of NAT ; ::_thesis: for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds
Proj (i,n) is_continuous_in x0
let x0 be Point of (REAL-NS n); ::_thesis: ( 1 <= i & i <= n implies Proj (i,n) is_continuous_in x0 )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: Proj (i,n) is_continuous_in x0
A2: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_(REAL-NS_n)_st_x1_in_dom_(Proj_(i,n))_&_||.(x1_-_x0).||_<_s_holds_
||.(((Proj_(i,n))_/._x1)_-_((Proj_(i,n))_/._x0)).||_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) ) )
assume A3: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) )
take s = r; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) )
thus 0 < s by A3; ::_thesis: for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r
now__::_thesis:_for_x1_being_Point_of_(REAL-NS_n)_st_x1_in_dom_(Proj_(i,n))_&_||.(x1_-_x0).||_<_s_holds_
||.(((Proj_(i,n))_/._x1)_-_((Proj_(i,n))_/._x0)).||_<_r
let x1 be Point of (REAL-NS n); ::_thesis: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s implies ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r )
assume A4: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r
(Proj (i,n)) /. (x1 - x0) = ((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0) by A1, PDIFF_8:11;
then ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| <= ||.(x1 - x0).|| by A1, PDIFF_8:3;
hence ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r by A4, XXREAL_0:2; ::_thesis: verum
end;
hence for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ; ::_thesis: verum
end;
hence Proj (i,n) is_continuous_in x0 by A2, NFCONT_1:7; ::_thesis: verum
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 )
proof
let x0 be real number ; ::_thesis: 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 )
let n be non empty Element of NAT ; ::_thesis: 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 )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( 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 )
hereby ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 )
assume A1: h is_continuous_in x0 ; ::_thesis: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0
then A2: x0 in dom h by NFCONT_3:7;
thus for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 )
assume i in Seg n ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0
then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A4: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
rng h c= the carrier of (REAL-NS n) ;
then A5: dom ((Proj (i,n)) * h) = dom h by A4, RELAT_1:27;
Proj (i,n) is_continuous_in h /. x0 by A3, Th45;
hence (Proj (i,n)) * h is_continuous_in x0 by A2, A5, A1, NFCONT_3:15; ::_thesis: verum
end;
end;
assume A6: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ; ::_thesis: h is_continuous_in x0
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then (Proj (1,n)) * h is_continuous_in x0 by A6;
then A7: x0 in dom ((Proj (1,n)) * h) by NFCONT_3:8;
A8: dom ((Proj (1,n)) * h) c= dom h by RELAT_1:25;
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 h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r ) )
proof
let r0 be Real; ::_thesis: ( 0 < r0 implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0 ) ) )
set r = r0 / 2;
assume A9: 0 < r0 ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0 ) )
then A10: 0 < r0 / 2 by XREAL_1:215;
defpred S1[ set , real number ] means ex j being Element of NAT st
( $1 = j & 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) );
A11: 0 < (r0 / 2) / n by A10, XREAL_1:139;
A12: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S1[j0,x]
proof
let j0 be Nat; ::_thesis: ( j0 in Seg n implies ex x being Element of REAL st S1[j0,x] )
assume A13: j0 in Seg n ; ::_thesis: ex x being Element of REAL st S1[j0,x]
reconsider j = j0 as Element of NAT by ORDINAL1:def_12;
A14: (Proj (j,n)) * h is_continuous_in x0 by A6, A13;
A15: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
rng h c= the carrier of (REAL-NS n) ;
then A16: dom ((Proj (j,n)) * h) = dom h by A15, RELAT_1:27;
consider sj being real number such that
A17: ( 0 < sj & ( for x1 being real number st x1 in dom ((Proj (j,n)) * h) & abs (x1 - x0) < sj holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A14, A11, NFCONT_3:8;
sj is Real by XREAL_0:def_1;
hence ex x being Element of REAL st S1[j0,x] by A17, A16; ::_thesis: verum
end;
consider s0 being FinSequence of REAL such that
A18: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A12);
n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A18, FUNCT_1:3;
rng s0 is finite by A18, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
A19: min rs0 in rng s0 by XXREAL_2:def_7;
then reconsider s = min rs0 as Real ;
take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0 ) )
consider i1 being set such that
A20: ( i1 in dom s0 & s = s0 . i1 ) by A19, FUNCT_1:def_3;
ex j being Element of NAT st
( i1 = j & 0 < s0 . i1 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . i1 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18, A20;
hence 0 < s by A20; ::_thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0
let x1 be real number ; ::_thesis: ( x1 in dom h & abs (x1 - x0) < s implies ||.((h /. x1) - (h /. x0)).|| < r0 )
assume A21: ( x1 in dom h & abs (x1 - x0) < s ) ; ::_thesis: ||.((h /. x1) - (h /. x0)).|| < r0
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
||.((Proj_(j,n))_._((h_/._x1)_-_(h_/._x0))).||_<=_(r0_/_2)_/_n
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n )
assume ( 1 <= j & j <= n ) ; ::_thesis: ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n
then A22: j in Seg n by FINSEQ_1:1;
then consider jj being Element of NAT such that
A23: ( jj = j & 0 < s0 . j & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . j holds
||.((((Proj (jj,n)) * h) /. x1) - (((Proj (jj,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18;
s0 . j in rng s0 by A22, A18, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def_7;
then abs (x1 - x0) < s0 . j by A21, XXREAL_0:2;
then A24: ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n by A23, A21;
A25: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
then A26: ((Proj (j,n)) * h) /. x1 = (Proj (j,n)) /. (h /. x1) by A21, PARTFUN2:4;
((Proj (j,n)) * h) /. x0 = (Proj (j,n)) /. (h /. x0) by A25, A8, A7, PARTFUN2:4;
hence ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n by A24, A26, PDIFF_8:11; ::_thesis: verum
end;
then ||.((h /. x1) - (h /. x0)).|| <= n * ((r0 / 2) / n) by PDIFF_8:16;
then A27: ||.((h /. x1) - (h /. x0)).|| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A9, XREAL_1:216;
hence ||.((h /. x1) - (h /. x0)).|| < r0 by A27, XXREAL_0:2; ::_thesis: verum
end;
hence h is_continuous_in x0 by A8, A7, NFCONT_3:8; ::_thesis: verum
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 )
proof
let n be non empty Element of NAT ; ::_thesis: 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 )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
hereby ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ) implies h is continuous )
assume A1: h is continuous ; ::_thesis: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous
thus for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is continuous )
assume A2: i in Seg n ; ::_thesis: (Proj (i,n)) * h is continuous
A3: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
rng h c= the carrier of (REAL-NS n) ;
then A4: dom ((Proj (i,n)) * h) = dom h by A3, RELAT_1:27;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_((Proj_(i,n))_*_h)_holds_
(Proj_(i,n))_*_h_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom ((Proj (i,n)) * h) implies (Proj (i,n)) * h is_continuous_in x0 )
assume x0 in dom ((Proj (i,n)) * h) ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0
then h is_continuous_in x0 by A1, A4, NFCONT_3:def_2;
hence (Proj (i,n)) * h is_continuous_in x0 by A2, Th46; ::_thesis: verum
end;
hence (Proj (i,n)) * h is continuous by NFCONT_3:def_2; ::_thesis: verum
end;
end;
assume A5: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ; ::_thesis: h is continuous
let x0 be real number ; :: according to NFCONT_3:def_2 ::_thesis: ( not x0 in dom h or h is_continuous_in x0 )
assume A6: x0 in dom h ; ::_thesis: h is_continuous_in x0
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(Proj_(i,n))_*_h_is_continuous_in_x0
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 )
assume A7: i in Seg n ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0
A8: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
rng h c= the carrier of (REAL-NS n) ;
then A9: dom ((Proj (i,n)) * h) = dom h by A8, RELAT_1:27;
(Proj (i,n)) * h is continuous by A5, A7;
hence (Proj (i,n)) * h is_continuous_in x0 by A6, A9, NFCONT_3:def_2; ::_thesis: verum
end;
hence h is_continuous_in x0 by Th46; ::_thesis: verum
end;