:: BHSP_2 semantic presentation

deffunc H₁( RealUnitarySpace) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is convergent means :Def1: :: BHSP_2:def 1
ex b₁ being Point of a₁ st
for b₂ being Real st b₂ > 0 holds
ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
dist (a₂ . b₄),b₁ < b₂;

end;

:: deftheorem Def1 defines convergent BHSP_2:def 1 :

theorem Th1: :: BHSP_2:1

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is V54 holds
b₂ is convergent

proof end;

theorem Th2: :: BHSP_2:2

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
b₃ . b₅ = b₂ . b₅ holds
b₃ is convergent

proof end;

theorem Th3: :: BHSP_2:3

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ + b₃ is convergent

proof end;

theorem Th4: :: BHSP_2:4

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ - b₃ is convergent

proof end;

theorem Th5: :: BHSP_2:5

for b₁ being RealUnitarySpace
for b₂ being Real
for b₃ being sequence of b₁ st b₃ is convergent holds
b₂ * b₃ is convergent

proof end;

theorem Th6: :: BHSP_2:6

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
- b₂ is convergent

proof end;

theorem Th7: :: BHSP_2:7

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ + b₂ is convergent

proof end;

theorem Th8: :: BHSP_2:8

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ - b₂ is convergent

proof end;

theorem Th9: :: BHSP_2:9

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is convergent iff ex b₃ being Point of b₁ st
for b₄ being Real st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₆ >= b₅ holds
||.((b₂ . b₆) - b₃).|| < b₄ )

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
assume E11: c₂ is convergent ;
func lim c₂ -> Point of a₁ means :Def2: :: BHSP_2:def 2
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
dist (a₂ . b₃),a₃ < b₁;
existence by E11, Def1;
uniqueness

proof end;

end;

:: deftheorem Def2 defines lim BHSP_2:def 2 :

theorem Th10: :: BHSP_2:10

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is V54 & b₂ in rng b₃ holds
lim b₃ = b₂

proof end;

theorem Th11: :: BHSP_2:11

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is V54 & ex b₄ being Nat st b₃ . b₄ = b₂ holds
lim b₃ = b₂

proof end;

theorem Th12: :: BHSP_2:12

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₃ . b₅ = b₂ . b₅ holds
lim b₂ = lim b₃

proof end;

theorem Th13: :: BHSP_2:13

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ + b₃) = (lim b₂) + (lim b₃)

proof end;

theorem Th14: :: BHSP_2:14

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ - b₃) = (lim b₂) - (lim b₃)

proof end;

theorem Th15: :: BHSP_2:15

for b₁ being RealUnitarySpace
for b₂ being Real
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₂ * b₃) = b₂ * (lim b₃)

proof end;

theorem Th16: :: BHSP_2:16

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
lim (- b₂) = - (lim b₂)

proof end;

theorem Th17: :: BHSP_2:17

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ + b₂) = (lim b₃) + b₂

proof end;

theorem Th18: :: BHSP_2:18

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ - b₂) = (lim b₃) - b₂

proof end;

theorem Th19: :: BHSP_2:19

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
( lim b₃ = b₂ iff for b₄ being Real st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₆ >= b₅ holds
||.((b₃ . b₆) - b₂).|| < b₄ )

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
func ||.c₂.|| -> Real_Sequence means :Def3: :: BHSP_2:def 3
for b₁ being Nat holds a₃ . b₁ = ||.(a₂ . b₁).||;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ||. BHSP_2:def 3 :

theorem Th20: :: BHSP_2:20

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
||.b₂.|| is convergent

proof end;

theorem Th21: :: BHSP_2:21

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.b₃.|| is convergent & lim ||.b₃.|| = ||.b₂.|| )

proof end;

theorem Th22: :: BHSP_2:22

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.(b₃ - b₂).|| is convergent & lim ||.(b₃ - b₂).|| = 0 )

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be sequence of c₁;
let c₃ be Point of c₁;
func dist c₂,c₃ -> Real_Sequence means :Def4: :: BHSP_2:def 4
for b₁ being Nat holds a₄ . b₁ = dist (a₂ . b₁),a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines dist BHSP_2:def 4 :

theorem Th23: :: BHSP_2:23

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
dist b₃,b₂ is convergent

proof end;

theorem Th24: :: BHSP_2:24

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( dist b₃,b₂ is convergent & lim (dist b₃,b₂) = 0 )

proof end;

theorem Th25: :: BHSP_2:25

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.(b₄ + b₅).|| is convergent & lim ||.(b₄ + b₅).|| = ||.(b₂ + b₃).|| )

proof end;

theorem Th26: :: BHSP_2:26

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.((b₄ + b₅) - (b₂ + b₃)).|| is convergent & lim ||.((b₄ + b₅) - (b₂ + b₃)).|| = 0 )

proof end;

theorem Th27: :: BHSP_2:27

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.(b₄ - b₅).|| is convergent & lim ||.(b₄ - b₅).|| = ||.(b₂ - b₃).|| )

proof end;

theorem Th28: :: BHSP_2:28

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.((b₄ - b₅) - (b₂ - b₃)).|| is convergent & lim ||.((b₄ - b₅) - (b₂ - b₃)).|| = 0 )

proof end;

theorem Th29: :: BHSP_2:29

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.(b₃ * b₄).|| is convergent & lim ||.(b₃ * b₄).|| = ||.(b₃ * b₂).|| )

proof end;

theorem Th30: :: BHSP_2:30

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.((b₃ * b₄) - (b₃ * b₂)).|| is convergent & lim ||.((b₃ * b₄) - (b₃ * b₂)).|| = 0 )

proof end;

theorem Th31: :: BHSP_2:31

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.(- b₃).|| is convergent & lim ||.(- b₃).|| = ||.(- b₂).|| )

proof end;

theorem Th32: :: BHSP_2:32

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.((- b₃) - (- b₂)).|| is convergent & lim ||.((- b₃) - (- b₂)).|| = 0 )

proof end;

Lemma26: for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.(b₄ + b₃).|| is convergent & lim ||.(b₄ + b₃).|| = ||.(b₂ + b₃).|| )

proof end;

theorem Th33: :: BHSP_2:33

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.((b₄ + b₃) - (b₂ + b₃)).|| is convergent & lim ||.((b₄ + b₃) - (b₂ + b₃)).|| = 0 )

proof end;

theorem Th34: :: BHSP_2:34

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.(b₄ - b₃).|| is convergent & lim ||.(b₄ - b₃).|| = ||.(b₂ - b₃).|| )

proof end;

theorem Th35: :: BHSP_2:35

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.((b₄ - b₃) - (b₂ - b₃)).|| is convergent & lim ||.((b₄ - b₃) - (b₂ - b₃)).|| = 0 )

proof end;

theorem Th36: :: BHSP_2:36

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( dist (b₄ + b₅),(b₂ + b₃) is convergent & lim (dist (b₄ + b₅),(b₂ + b₃)) = 0 )

proof end;

theorem Th37: :: BHSP_2:37

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( dist (b₄ - b₅),(b₂ - b₃) is convergent & lim (dist (b₄ - b₅),(b₂ - b₃)) = 0 )

proof end;

theorem Th38: :: BHSP_2:38

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( dist (b₃ * b₄),(b₃ * b₂) is convergent & lim (dist (b₃ * b₄),(b₃ * b₂)) = 0 )

proof end;

theorem Th39: :: BHSP_2:39

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( dist (b₄ + b₃),(b₂ + b₃) is convergent & lim (dist (b₄ + b₃),(b₂ + b₃)) = 0 )

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be Real;
func Ball c₂,c₃ -> Subset of a₁ equals :: BHSP_2:def 5
{ b₁ where B is Point of a₁ : ||.(a₂ - b₁).|| < a₃ } ;
coherence

proof end;

func cl_Ball c₂,c₃ -> Subset of a₁ equals :: BHSP_2:def 6
{ b₁ where B is Point of a₁ : ||.(a₂ - b₁).|| <= a₃ } ;
coherence

proof end;

func Sphere c₂,c₃ -> Subset of a₁ equals :: BHSP_2:def 7
{ b₁ where B is Point of a₁ : ||.(a₂ - b₁).|| = a₃ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines Ball BHSP_2:def 5 :

:: deftheorem Def6 defines cl_Ball BHSP_2:def 6 :

:: deftheorem Def7 defines Sphere BHSP_2:def 7 :

theorem Th40: :: BHSP_2:40

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Ball b₃,b₄ iff ||.(b₃ - b₂).|| < b₄ )

proof end;

theorem Th41: :: BHSP_2:41

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Ball b₃,b₄ iff dist b₃,b₂ < b₄ )

proof end;

theorem Th42: :: BHSP_2:42

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real st b₃ > 0 holds
b₂ in Ball b₂,b₃

proof end;

theorem Th43: :: BHSP_2:43

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₂ in Ball b₃,b₅ & b₄ in Ball b₃,b₅ holds
dist b₂,b₄ < 2 * b₅

proof end;

theorem Th44: :: BHSP_2:44

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₂ in Ball b₃,b₅ holds
b₂ - b₄ in Ball (b₃ - b₄),b₅

proof end;

theorem Th45: :: BHSP_2:45

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₂ in Ball b₃,b₄ holds
b₂ - b₃ in Ball (0. b₁),b₄

proof end;

theorem Th46: :: BHSP_2:46

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Real st b₂ in Ball b₃,b₄ & b₄ <= b₅ holds
b₂ in Ball b₃,b₅

proof end;

theorem Th47: :: BHSP_2:47

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in cl_Ball b₃,b₄ iff ||.(b₃ - b₂).|| <= b₄ )

proof end;

theorem Th48: :: BHSP_2:48

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in cl_Ball b₃,b₄ iff dist b₃,b₂ <= b₄ )

proof end;

theorem Th49: :: BHSP_2:49

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real st b₃ >= 0 holds
b₂ in cl_Ball b₂,b₃

proof end;

theorem Th50: :: BHSP_2:50

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₂ in Ball b₃,b₄ holds
b₂ in cl_Ball b₃,b₄

proof end;

theorem Th51: :: BHSP_2:51

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Sphere b₃,b₄ iff ||.(b₃ - b₂).|| = b₄ )

proof end;

theorem Th52: :: BHSP_2:52

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Sphere b₃,b₄ iff dist b₃,b₂ = b₄ )

proof end;

theorem Th53: :: BHSP_2:53

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₂ in Sphere b₃,b₄ holds
b₂ in cl_Ball b₃,b₄

proof end;

theorem Th54: :: BHSP_2:54

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds Ball b₂,b₃ c= cl_Ball b₂,b₃

proof end;

theorem Th55: :: BHSP_2:55

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds Sphere b₂,b₃ c= cl_Ball b₂,b₃

proof end;

theorem Th56: :: BHSP_2:56

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds (Ball b₂,b₃) \/ (Sphere b₂,b₃) = cl_Ball b₂,b₃

proof end;