:: More on the Continuity of Real Functions
:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama
::
:: Received February 22, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users

definition

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

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

end;

:: deftheorem defines is_continuous_in NFCONT_4:def 1 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being Real 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 :: NFCONT_4:1

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

theorem Th2: :: NFCONT_4:2

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

proof end;

theorem Th3: :: NFCONT_4:3

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

proof end;

theorem Th4: :: NFCONT_4:4

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

proof end;

definition

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

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

existence
ex b₁ being PartFunc of Z,REAL st
( dom b₁ = dom f & ( for x being set st x in dom b₁ holds
b₁ /. x = |.(f /. x).| ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of Z,REAL st dom b₁ = dom f & ( for x being set st x in dom b₁ holds
b₁ /. x = |.(f /. x).| ) & dom b₂ = dom f & ( for x being set st x in dom b₂ holds
b₂ /. x = |.(f /. x).| ) holds
b₁ = b₂

proof 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 b₄ being PartFunc of Z,REAL holds
( b₄ = |.f.| iff ( dom b₄ = dom f & ( for x being set st x in dom b₄ holds
b₄ /. 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 H₁( set ) -> M14( REAL , REAL n) = - (f /. $1);
defpred S₁[ set ] means $1 in dom f;

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

existence
ex b₁ being PartFunc of Z,(REAL n) st
( dom b₁ = dom f & ( for c being set st c in dom b₁ holds
b₁ /. c = - (f /. c) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of Z,(REAL n) st dom b₁ = dom f & ( for c being set st c in dom b₁ holds
b₁ /. c = - (f /. c) ) & dom b₂ = dom f & ( for c being set st c in dom b₂ holds
b₂ /. c = - (f /. c) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines - NFCONT_4:def 3 :
for n being Element of NAT
for Z being non empty set
for f, b₄ being PartFunc of Z,(REAL n) holds
( b₄ = - f iff ( dom b₄ = dom f & ( for c being set st c in dom b₄ holds
b₄ /. 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 end;

theorem Th6: :: NFCONT_4:6

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

proof end;

theorem :: 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 end;

theorem Th8: :: NFCONT_4:8

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

proof end;

theorem Th9: :: NFCONT_4:9

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

proof end;

theorem Th10: :: NFCONT_4:10

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

proof end;

theorem :: NFCONT_4:11

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

proof end;

theorem :: NFCONT_4:12

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

proof end;

theorem :: NFCONT_4:13

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

proof end;

theorem :: NFCONT_4:14

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

proof end;

theorem :: NFCONT_4:15

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

proof end;

theorem :: NFCONT_4:16

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

proof end;

theorem :: NFCONT_4:17

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

proof end;

theorem :: NFCONT_4:18

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

proof end;

theorem :: NFCONT_4:19

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

proof end;

theorem Th20: :: NFCONT_4:20

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

proof end;

definition

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

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

end;

:: deftheorem defines is_continuous_in NFCONT_4:def 4 :
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 :: NFCONT_4:21

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

theorem Th22: :: NFCONT_4:22

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

proof end;

definition

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

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

end;

:: deftheorem Def5 defines continuous NFCONT_4:def 5 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is continuous iff for x0 being Real 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 end;

theorem Th24: :: NFCONT_4:24

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

proof end;

registration

let n be Element of NAT ;

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ is constant holds
b₁ is continuous

proof end;

end;

registration

let n be Element of NAT ;

cluster Relation-like REAL -defined REAL n -valued Function-like V158() V231() V232() V233() continuous for Element of bool [:REAL,(REAL n):];

existence
ex b₁ being PartFunc of REAL,(REAL n) st b₁ is continuous

proof end;

end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = f | X holds
b₁ is continuous

proof end;

end;

theorem :: NFCONT_4:25

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

proof end;

registration

let n be Element of NAT ;

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ is empty holds
b₁ is continuous ;

end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = f | X holds
b₁ is continuous

proof end;

end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = f1 + f2 holds
b₁ is continuous

proof end;

end;

theorem :: NFCONT_4:26

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

proof end;

theorem :: NFCONT_4:27

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

proof end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = r (#) f holds
b₁ is continuous

proof end;

end;

theorem :: NFCONT_4:28

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

proof end;

theorem :: NFCONT_4:29

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

theorem :: NFCONT_4:30

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

proof end;

theorem :: NFCONT_4:31

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

proof end;

theorem :: NFCONT_4:32

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

proof end;

definition

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

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

end;

:: deftheorem defines Lipschitzian NFCONT_4:def 6 :
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 st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) )

proof end;

theorem Th34: :: NFCONT_4:34

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

theorem :: NFCONT_4:35

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 st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) )

proof end;

registration

let n be Element of NAT ;

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ is empty holds
b₁ is Lipschitzian

proof end;

end;

registration

let n be Element of NAT ;

cluster Relation-like REAL -defined REAL n -valued empty Function-like V158() V231() V232() V233() for Element of bool [:REAL,(REAL n):];

existence
ex b₁ being PartFunc of REAL,(REAL n) st b₁ is empty

proof end;

end;

registration

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

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

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

proof end;

end;

theorem :: NFCONT_4:36

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

proof end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = f1 + f2 holds
b₁ is Lipschitzian

proof end;

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = f1 - f2 holds
b₁ is Lipschitzian

proof end;

end;

theorem :: NFCONT_4:37

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

proof end;

theorem :: NFCONT_4:38

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

proof end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ = p (#) f holds
b₁ is Lipschitzian

proof end;

end;

theorem :: NFCONT_4:39

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

proof end;

registration

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

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

coherence
for b₁ being PartFunc of REAL,REAL st b₁ = |.f.| holds
b₁ is Lipschitzian

proof 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 end;

registration

let n be Element of NAT ;

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ is constant holds
b₁ is Lipschitzian

proof end;

end;

registration

let n be Element of NAT ;

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

coherence
for b₁ being PartFunc of REAL,(REAL n) st b₁ is Lipschitzian holds
b₁ is continuous by Th23;

end;

theorem :: NFCONT_4:41

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

proof end;

theorem Th42: :: NFCONT_4:42

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

proof end;

theorem Th43: :: NFCONT_4:43

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

proof end;

theorem :: NFCONT_4:44

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

proof end;

theorem Th45: :: NFCONT_4:45

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

proof end;

theorem Th46: :: NFCONT_4:46

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

proof end;

theorem :: NFCONT_4:47

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

proof end;