:: NFCONT_1 semantic presentation

definition

let c₁, c₂ be 1-sorted ;
mode PartFunc of a₁,a₂ is PartFunc of the carrier of a₁,the carrier of a₂;

end;

definition

let c₁ be RealLinearSpace;
let c₂ be sequence of c₁;
func - c₂ -> sequence of a₁ means :Def1: :: NFCONT_1:def 1
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines - NFCONT_1:def 1 :

theorem Th1: :: NFCONT_1:1

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th2: :: NFCONT_1:2

for b₁ being RealNormSpace
for b₂ being sequence of b₁ holds - b₂ = (- 1) * b₂

proof end;

definition

let c₁, c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
func ||.c₃.|| -> PartFunc of the carrier of a₁, REAL means :Def2: :: NFCONT_1:def 2
( dom a₄ = dom a₃ & ( for b₁ being Point of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = ||.(a₃ /. b₁).|| ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be RealNormSpace;
let c₂ be Point of c₁;
mode Neighbourhood of c₂ -> Subset of a₁ means :Def3: :: NFCONT_1:def 3
ex b₁ being Real st
( 0 < b₁ & { b₂ where B is Point of a₁ : ||.(b₂ - a₂).|| < b₁ } c= a₃ );
existence

proof end;

end;

:: deftheorem Def3 defines Neighbourhood NFCONT_1:def 3 :

theorem Th3: :: NFCONT_1:3

for b₁ being RealNormSpace
for b₂ being Point of b₁
for b₃ being Real st 0 < b₃ holds
{ b₄ where B is Point of b₁ : ||.(b₄ - b₂).|| < b₃ } is Neighbourhood of b₂

proof end;

theorem Th4: :: NFCONT_1:4

for b₁ being RealNormSpace
for b₂ being Point of b₁
for b₃ being Neighbourhood of b₂ holds b₂ in b₃

proof end;

definition

let c₁ be RealNormSpace;
let c₂ be Subset of c₁;
attr a₂ is compact means :Def4: :: NFCONT_1:def 4
for b₁ being sequence of a₁ st rng b₁ c= a₂ holds
ex b₂ being sequence of a₁ st
( b₂ is subsequence of b₁ & b₂ is convergent & lim b₂ in a₂ );

end;

:: deftheorem Def4 defines compact NFCONT_1:def 4 :

definition

let c₁ be RealNormSpace;
let c₂ be Subset of c₁;
attr a₂ is closed means :: NFCONT_1:def 5
for b₁ being sequence of a₁ st rng b₁ c= a₂ & b₁ is convergent holds
lim b₁ in a₂;

end;

:: deftheorem Def5 defines closed NFCONT_1:def 5 :

definition

let c₁ be RealNormSpace;
let c₂ be Subset of c₁;
attr a₂ is open means :: NFCONT_1:def 6
a₂ ` is closed;

end;

:: deftheorem Def6 defines open NFCONT_1:def 6 :

definition

let c₁, c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be sequence of c₁;
assume E8: rng c₄ c= dom c₃ ;
func c₃ * c₄ -> sequence of a₂ equals :Def7: :: NFCONT_1:def 7
a₃ * a₄;
coherence

proof end;

end;

:: deftheorem Def7 defines * NFCONT_1:def 7 :

definition

let c₁ be RealNormSpace;
let c₂ be PartFunc of the carrier of c₁, REAL ;
let c₃ be sequence of c₁;
assume E9: rng c₃ c= dom c₂ ;
func c₂ * c₃ -> Real_Sequence equals :Def8: :: NFCONT_1:def 8
a₂ * a₃;
coherence

proof end;

end;

:: deftheorem Def8 defines * NFCONT_1:def 8 :

definition

let c₁, c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be Point of c₁;
pred c₃ is_continuous_in c₄ means :Def9: :: NFCONT_1:def 9
( a₄ in dom a₃ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₃ & b₁ is convergent & lim b₁ = a₄ holds
( a₃ * b₁ is convergent & a₃ /. a₄ = lim (a₃ * b₁) ) ) );

end;

:: deftheorem Def9 defines is_continuous_in NFCONT_1:def 9 :

definition

let c₁ be RealNormSpace;
let c₂ be PartFunc of the carrier of c₁, REAL ;
let c₃ be Point of c₁;
pred c₂ is_continuous_in c₃ means :Def10: :: NFCONT_1:def 10
( a₃ in dom a₂ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₂ & b₁ is convergent & lim b₁ = a₃ holds
( a₂ * b₁ is convergent & a₂ /. a₃ = lim (a₂ * b₁) ) ) );

end;

:: deftheorem Def10 defines is_continuous_in NFCONT_1:def 10 :

theorem Th5: :: NFCONT_1:5

for b₁ being Nat
for b₂, b₃ being RealNormSpace
for b₄ being sequence of b₂
for b₅ being PartFunc of b₂,b₃ st rng b₄ c= dom b₅ holds
b₄ . b₁ in dom b₅

proof end;

theorem Th6: :: NFCONT_1:6

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being set holds
( b₃ in rng b₂ iff ex b₄ being Nat st b₃ = b₂ . b₄ )

proof end;

theorem Th7: :: NFCONT_1:7

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₃ is subsequence of b₂ holds
rng b₃ c= rng b₂

proof end;

theorem Th8: :: NFCONT_1:8

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being sequence of b₂ st rng b₄ c= dom b₃ holds
for b₅ being Nat holds (b₃ * b₄) . b₅ = b₃ /. (b₄ . b₅)

proof end;

theorem Th9: :: NFCONT_1:9

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being sequence of b₁ st rng b₃ c= dom b₂ holds
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ /. (b₃ . b₄)

proof end;

theorem Th10: :: NFCONT_1:10

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁
for b₅ being increasing Seq_of_Nat st rng b₄ c= dom b₃ holds
(b₃ * b₄) * b₅ = b₃ * (b₄ * b₅)

proof end;

theorem Th11: :: NFCONT_1:11

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being sequence of b₁
for b₄ being increasing Seq_of_Nat st rng b₃ c= dom b₂ holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th12: :: NFCONT_1:12

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄, b₅ being sequence of b₁ st rng b₄ c= dom b₃ & b₅ is subsequence of b₄ holds
b₃ * b₅ is subsequence of b₃ * b₄

proof end;

theorem Th13: :: NFCONT_1:13

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃, b₄ being sequence of b₁ st rng b₃ c= dom b₂ & b₄ is subsequence of b₃ holds
b₂ * b₄ is subsequence of b₂ * b₃

proof end;

theorem Th14: :: NFCONT_1:14

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Real st 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₂ st b₇ in dom b₃ & ||.(b₇ - b₄).|| < b₆ holds
||.((b₃ /. b₇) - (b₃ /. b₄)).|| < b₅ ) ) ) ) )

proof end;

theorem Th15: :: NFCONT_1:15

for b₁ being RealNormSpace
for b₂ being Point of b₁
for b₃ being PartFunc of the carrier of b₁, REAL holds
( b₃ is_continuous_in b₂ iff ( b₂ in dom b₃ & ( for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( 0 < b₅ & ( for b₆ being Point of b₁ st b₆ in dom b₃ & ||.(b₆ - b₂).|| < b₅ holds
abs ((b₃ /. b₆) - (b₃ /. b₂)) < b₄ ) ) ) ) )

proof end;

theorem Th16: :: NFCONT_1:16

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Neighbourhood of b₃ /. b₄ ex b₆ being Neighbourhood of b₄ st
for b₇ being Point of b₂ st b₇ in dom b₃ & b₇ in b₆ holds
b₃ /. b₇ in b₅ ) ) )

proof end;

theorem Th17: :: NFCONT_1:17

proof end;

theorem Th18: :: NFCONT_1:18

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₄ in dom b₃ & ex b₅ being Neighbourhood of b₄ st (dom b₃) /\ b₅ = {b₄} holds
b₃ is_continuous_in b₄

proof end;

theorem Th19: :: NFCONT_1:19

for b₁, b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being sequence of b₁ st rng b₅ c= (dom b₃) /\ (dom b₄) holds
( (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅) & (b₃ - b₄) * b₅ = (b₃ * b₅) - (b₄ * b₅) )

proof end;

theorem Th20: :: NFCONT_1:20

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁
for b₅ being Real st rng b₄ c= dom b₃ holds
(b₅ (#) b₃) * b₄ = b₅ * (b₃ * b₄)

proof end;

theorem Th21: :: NFCONT_1:21

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁ st rng b₄ c= dom b₃ holds
( ||.(b₃ * b₄).|| = ||.b₃.|| * b₄ & - (b₃ * b₄) = (- b₃) * b₄ )

proof end;

theorem Th22: :: NFCONT_1:22

for b₁, b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₂,b₁
for b₅ being Point of b₂ st b₃ is_continuous_in b₅ & b₄ is_continuous_in b₅ holds
( b₃ + b₄ is_continuous_in b₅ & b₃ - b₄ is_continuous_in b₅ )

proof end;

theorem Th23: :: NFCONT_1:23

for b₁ being Real
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₃,b₂
for b₅ being Point of b₃ st b₄ is_continuous_in b₅ holds
b₁ (#) b₄ is_continuous_in b₅

proof end;

theorem Th24: :: NFCONT_1:24

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₃ is_continuous_in b₄ holds
( ||.b₃.|| is_continuous_in b₄ & - b₃ is_continuous_in b₄ )

proof end;

definition

let c₁, c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
pred c₃ is_continuous_on c₄ means :Def11: :: NFCONT_1:def 11
( a₄ c= dom a₃ & ( for b₁ being Point of a₁ st b₁ in a₄ holds
a₃ | a₄ is_continuous_in b₁ ) );

end;

:: deftheorem Def11 defines is_continuous_on NFCONT_1:def 11 :

definition

let c₁ be RealNormSpace;
let c₂ be PartFunc of the carrier of c₁, REAL ;
let c₃ be set ;
pred c₂ is_continuous_on c₃ means :Def12: :: NFCONT_1:def 12
( a₃ c= dom a₂ & ( for b₁ being Point of a₁ st b₁ in a₃ holds
a₂ | a₃ is_continuous_in b₁ ) );

end;

:: deftheorem Def12 defines is_continuous_on NFCONT_1:def 12 :

theorem Th25: :: NFCONT_1:25

for b₁, b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being sequence of b₂ st rng b₅ c= b₃ & b₅ is convergent & lim b₅ in b₃ holds
( b₄ * b₅ is convergent & b₄ /. (lim b₅) = lim (b₄ * b₅) ) ) ) )

proof end;

theorem Th26: :: NFCONT_1:26

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₃,b₂ holds
( b₄ is_continuous_on b₁ iff ( b₁ c= dom b₄ & ( for b₅ being Point of b₃
for b₆ being Real st b₅ in b₁ & 0 < b₆ holds
ex b₇ being Real st
( 0 < b₇ & ( for b₈ being Point of b₃ st b₈ in b₁ & ||.(b₈ - b₅).|| < b₇ holds
||.((b₄ /. b₈) - (b₄ /. b₅)).|| < b₆ ) ) ) ) )

proof end;

theorem Th27: :: NFCONT_1:27

for b₁ being set
for b₂ being RealNormSpace
for b₃ being PartFunc of the carrier of b₂, REAL holds
( b₃ is_continuous_on b₁ iff ( b₁ c= dom b₃ & ( for b₄ being Point of b₂
for b₅ being Real st b₄ in b₁ & 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₂ st b₇ in b₁ & ||.(b₇ - b₄).|| < b₆ holds
abs ((b₃ /. b₇) - (b₃ /. b₄)) < b₅ ) ) ) ) )

proof end;

theorem Th28: :: NFCONT_1:28

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ holds
( b₄ is_continuous_on b₁ iff b₄ | b₁ is_continuous_on b₁ )

proof end;

theorem Th29: :: NFCONT_1:29

for b₁ being set
for b₂ being RealNormSpace
for b₃ being PartFunc of the carrier of b₂, REAL holds
( b₃ is_continuous_on b₁ iff b₃ | b₁ is_continuous_on b₁ )

proof end;

theorem Th30: :: NFCONT_1:30

for b₁, b₂ being set
for b₃, b₄ being RealNormSpace
for b₅ being PartFunc of b₃,b₄ st b₅ is_continuous_on b₁ & b₂ c= b₁ holds
b₅ is_continuous_on b₂

proof end;

theorem Th31: :: NFCONT_1:31

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₄ in dom b₃ holds
b₃ is_continuous_on {b₄}

proof end;

theorem Th32: :: NFCONT_1:32

for b₁, b₂ being RealNormSpace
for b₃ being set
for b₄, b₅ being PartFunc of b₂,b₁ st b₄ is_continuous_on b₃ & b₅ is_continuous_on b₃ holds
( b₄ + b₅ is_continuous_on b₃ & b₄ - b₅ is_continuous_on b₃ )

proof end;

theorem Th33: :: NFCONT_1:33

for b₁, b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₂,b₁ st b₅ is_continuous_on b₃ & b₆ is_continuous_on b₄ holds
( b₅ + b₆ is_continuous_on b₃ /\ b₄ & b₅ - b₆ is_continuous_on b₃ /\ b₄ )

proof end;

theorem Th34: :: NFCONT_1:34

for b₁, b₂ being RealNormSpace
for b₃ being Real
for b₄ being set
for b₅ being PartFunc of b₂,b₁ st b₅ is_continuous_on b₄ holds
b₃ (#) b₅ is_continuous_on b₄

proof end;

theorem Th35: :: NFCONT_1:35

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_continuous_on b₁ holds
( ||.b₄.|| is_continuous_on b₁ & - b₄ is_continuous_on b₁ )

proof end;

theorem Th36: :: NFCONT_1:36

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st b₃ is total & ( for b₄, b₅ being Point of b₂ holds b₃ /. (b₄ + b₅) = (b₃ /. b₄) + (b₃ /. b₅) ) & ex b₄ being Point of b₂ st b₃ is_continuous_in b₄ holds
b₃ is_continuous_on the carrier of b₂

proof end;

theorem Th37: :: NFCONT_1:37

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
rng b₃ is compact

proof end;

theorem Th38: :: NFCONT_1:38

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL st dom b₂ is compact & b₂ is_continuous_on dom b₂ holds
rng b₂ is compact

proof end;

theorem Th39: :: NFCONT_1:39

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Subset of b₂ st b₄ c= dom b₃ & b₄ is compact & b₃ is_continuous_on b₄ holds
b₃ .: b₄ is compact

proof end;

theorem Th40: :: NFCONT_1:40

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL st dom b₂ <> {} & dom b₂ is compact & b₂ is_continuous_on dom b₂ holds
ex b₃, b₄ being Point of b₁ st
( b₃ in dom b₂ & b₄ in dom b₂ & b₂ /. b₃ = upper_bound (rng b₂) & b₂ /. b₄ = lower_bound (rng b₂) )

proof end;

theorem Th41: :: NFCONT_1:41

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st dom b₃ <> {} & dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
ex b₄, b₅ being Point of b₂ st
( b₄ in dom b₃ & b₅ in dom b₃ & ||.b₃.|| /. b₄ = upper_bound (rng ||.b₃.||) & ||.b₃.|| /. b₅ = lower_bound (rng ||.b₃.||) )

proof end;

theorem Th42: :: NFCONT_1:42

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ holds ||.b₄.|| | b₁ = ||.(b₄ | b₁).||

proof end;

theorem Th43: :: NFCONT_1:43

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Subset of b₂ st b₄ <> {} & b₄ c= dom b₃ & b₄ is compact & b₃ is_continuous_on b₄ holds
ex b₅, b₆ being Point of b₂ st
( b₅ in b₄ & b₆ in b₄ & ||.b₃.|| /. b₅ = upper_bound (||.b₃.|| .: b₄) & ||.b₃.|| /. b₆ = lower_bound (||.b₃.|| .: b₄) )

proof end;

theorem Th44: :: NFCONT_1:44

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being Subset of b₁ st b₃ <> {} & b₃ c= dom b₂ & b₃ is compact & b₂ is_continuous_on b₃ holds
ex b₄, b₅ being Point of b₁ st
( b₄ in b₃ & b₅ in b₃ & b₂ /. b₄ = upper_bound (b₂ .: b₃) & b₂ /. b₅ = lower_bound (b₂ .: b₃) )

proof end;

definition

let c₁, c₂ be RealNormSpace;
let c₃ be set ;
let c₄ be PartFunc of c₁,c₂;
pred c₄ is_Lipschitzian_on c₃ means :Def13: :: NFCONT_1:def 13
( a₃ c= dom a₄ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₃ & b₃ in a₃ holds
||.((a₄ /. b₂) - (a₄ /. b₃)).|| <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def13 defines is_Lipschitzian_on NFCONT_1:def 13 :

definition

let c₁ be RealNormSpace;
let c₂ be set ;
let c₃ be PartFunc of the carrier of c₁, REAL ;
pred c₃ is_Lipschitzian_on c₂ means :Def14: :: NFCONT_1:def 14
( a₂ c= dom a₃ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₂ & b₃ in a₂ holds
abs ((a₃ /. b₂) - (a₃ /. b₃)) <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def14 defines is_Lipschitzian_on NFCONT_1:def 14 :

theorem Th45: :: NFCONT_1:45

for b₁, b₂ being set
for b₃, b₄ being RealNormSpace
for b₅ being PartFunc of b₃,b₄ st b₅ is_Lipschitzian_on b₁ & b₂ c= b₁ holds
b₅ is_Lipschitzian_on b₂

proof end;

theorem Th46: :: NFCONT_1:46

for b₁, b₂ being set
for b₃, b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,b₄ st b₅ is_Lipschitzian_on b₁ & b₆ is_Lipschitzian_on b₂ holds
b₅ + b₆ is_Lipschitzian_on b₁ /\ b₂

proof end;

theorem Th47: :: NFCONT_1:47

for b₁, b₂ being set
for b₃, b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,b₄ st b₅ is_Lipschitzian_on b₁ & b₆ is_Lipschitzian_on b₂ holds
b₅ - b₆ is_Lipschitzian_on b₁ /\ b₂

proof end;

theorem Th48: :: NFCONT_1:48

for b₁ being set
for b₂ being Real
for b₃, b₄ being RealNormSpace
for b₅ being PartFunc of b₃,b₄ st b₅ is_Lipschitzian_on b₁ holds
b₂ (#) b₅ is_Lipschitzian_on b₁

proof end;

theorem Th49: :: NFCONT_1:49

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_Lipschitzian_on b₁ holds
( - b₄ is_Lipschitzian_on b₁ & ||.b₄.|| is_Lipschitzian_on b₁ )

proof end;

theorem Th50: :: NFCONT_1:50

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₁ c= dom b₄ & b₄ is_constant_on b₁ holds
b₄ is_Lipschitzian_on b₁

proof end;

theorem Th51: :: NFCONT_1:51

for b₁ being RealNormSpace
for b₂ being Subset of b₁ holds id b₂ is_Lipschitzian_on b₂

proof end;

theorem Th52: :: NFCONT_1:52

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_Lipschitzian_on b₁ holds
b₄ is_continuous_on b₁

proof end;

theorem Th53: :: NFCONT_1:53

for b₁ being set
for b₂ being RealNormSpace
for b₃ being PartFunc of the carrier of b₂, REAL st b₃ is_Lipschitzian_on b₁ holds
b₃ is_continuous_on b₁

proof end;

theorem Th54: :: NFCONT_1:54

for b₁, b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st ex b₄ being Point of b₁ st rng b₃ = {b₄} holds
b₃ is_continuous_on dom b₃

proof end;

theorem Th55: :: NFCONT_1:55

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₁ c= dom b₄ & b₄ is_constant_on b₁ holds
b₄ is_continuous_on b₁

proof end;

theorem Th56: :: NFCONT_1:56

for b₁ being RealNormSpace
for b₂ being PartFunc of b₁,b₁ st ( for b₃ being Point of b₁ st b₃ in dom b₂ holds
b₂ /. b₃ = b₃ ) holds
b₂ is_continuous_on dom b₂

proof end;

theorem Th57: :: NFCONT_1:57

for b₁ being RealNormSpace
for b₂ being PartFunc of b₁,b₁ st b₂ = id (dom b₂) holds
b₂ is_continuous_on dom b₂

proof end;

theorem Th58: :: NFCONT_1:58

for b₁ being RealNormSpace
for b₂ being Subset of b₁
for b₃ being PartFunc of b₁,b₁ st b₂ c= dom b₃ & b₃ | b₂ = id b₂ holds
b₃ is_continuous_on b₂

proof end;

theorem Th59: :: NFCONT_1:59

for b₁ being set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₂
for b₄ being Real
for b₅ being Point of b₂ st b₁ c= dom b₃ & ( for b₆ being Point of b₂ st b₆ in b₁ holds
b₃ /. b₆ = (b₄ * b₆) + b₅ ) holds
b₃ is_continuous_on b₁

proof end;

theorem Th60: :: NFCONT_1:60

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL st ( for b₃ being Point of b₁ st b₃ in dom b₂ holds
b₂ /. b₃ = ||.b₃.|| ) holds
b₂ is_continuous_on dom b₂

proof end;

theorem Th61: :: NFCONT_1:61

for b₁ being set
for b₂ being RealNormSpace
for b₃ being PartFunc of the carrier of b₂, REAL st b₁ c= dom b₃ & ( for b₄ being Point of b₂ st b₄ in b₁ holds
b₃ /. b₄ = ||.b₄.|| ) holds
b₃ is_continuous_on b₁

proof end;