:: RUSUB_5 semantic presentation

definition

let c₁ be non empty RLSStruct ;
let c₂, c₃ be Affine Subset of c₁;
pred c₂ is_parallel_to c₃ means :Def1: :: RUSUB_5:def 1
ex b₁ being VECTOR of a₁ st a₂ = a₃ + {b₁};

end;

:: deftheorem Def1 defines is_parallel_to RUSUB_5:def 1 :

theorem Th1: :: RUSUB_5:1

for b₁ being non empty right_zeroed RLSStruct
for b₂ being Affine Subset of b₁ holds b₂ is_parallel_to b₂

proof end;

theorem Th2: :: RUSUB_5:2

for b₁ being non empty add-associative right_zeroed right_complementable RLSStruct
for b₂, b₃ being Affine Subset of b₁ st b₂ is_parallel_to b₃ holds
b₃ is_parallel_to b₂

proof end;

theorem Th3: :: RUSUB_5:3

for b₁ being non empty Abelian add-associative right_zeroed right_complementable RLSStruct
for b₂, b₃, b₄ being Affine Subset of b₁ st b₂ is_parallel_to b₃ & b₃ is_parallel_to b₄ holds
b₂ is_parallel_to b₄

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Subset of c₁;
func c₂ - c₃ -> Subset of a₁ equals :: RUSUB_5:def 2
{ (b₁ - b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines - RUSUB_5:def 2 :

theorem Th4: :: RUSUB_5:4

for b₁ being RealLinearSpace
for b₂, b₃ being Affine Subset of b₁ holds b₂ - b₃ is Affine

proof end;

theorem Th5: :: RUSUB_5:5

for b₁ being non empty LoopStr
for b₂, b₃ being Subset of b₁ st ( b₂ is empty or b₃ is empty ) holds
b₂ + b₃ is empty

proof end;

theorem Th6: :: RUSUB_5:6

for b₁ being non empty LoopStr
for b₂, b₃ being non empty Subset of b₁ holds not b₂ + b₃ is empty

proof end;

theorem Th7: :: RUSUB_5:7

for b₁ being non empty LoopStr
for b₂, b₃ being Subset of b₁ st ( b₂ is empty or b₃ is empty ) holds
b₂ - b₃ is empty

proof end;

theorem Th8: :: RUSUB_5:8

for b₁ being non empty LoopStr
for b₂, b₃ being non empty Subset of b₁ holds not b₂ - b₃ is empty

proof end;

theorem Th9: :: RUSUB_5:9

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ holds
( b₂ = b₃ + {b₄} iff b₂ - {b₄} = b₃ )

proof end;

theorem Th10: :: RUSUB_5:10

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₄ in b₃ holds
b₂ + {b₄} c= b₂ + b₃

proof end;

theorem Th11: :: RUSUB_5:11

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₄ in b₃ holds
b₂ - {b₄} c= b₂ - b₃

proof end;

theorem Th12: :: RUSUB_5:12

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ holds 0. b₁ in b₂ - b₂

proof end;

theorem Th13: :: RUSUB_5:13

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁
for b₃ being VECTOR of b₁ st b₂ is Subspace-like & b₃ in b₂ holds
b₂ + {b₃} c= b₂

proof end;

theorem Th14: :: RUSUB_5:14

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being non empty Affine Subset of b₁ st b₃ is Subspace-like & b₄ is Subspace-like & b₂ is_parallel_to b₃ & b₂ is_parallel_to b₄ holds
b₃ = b₄

proof end;

theorem Th15: :: RUSUB_5:15

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
0. b₁ in b₂ - {b₃}

proof end;

theorem Th16: :: RUSUB_5:16

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
ex b₄ being non empty Affine Subset of b₁ st
( b₄ = b₂ - {b₃} & b₂ is_parallel_to b₄ & b₄ is Subspace-like )

proof end;

theorem Th17: :: RUSUB_5:17

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁
for b₃, b₄ being VECTOR of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₂ - {b₄} = b₂ - {b₃}

proof end;

theorem Th18: :: RUSUB_5:18

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁ holds b₂ - b₂ = union { (b₂ - {b₃}) where B is VECTOR of b₁ : b₃ in b₂ }

proof end;

theorem Th19: :: RUSUB_5:19

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
b₂ - {b₃} = union { (b₂ - {b₄}) where B is VECTOR of b₁ : b₄ in b₂ }

proof end;

theorem Th20: :: RUSUB_5:20

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁ ex b₃ being non empty Affine Subset of b₁ st
( b₃ = b₂ - b₂ & b₃ is Subspace-like & b₂ is_parallel_to b₃ )

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Subspace of c₁;
func Ort_Comp c₂ -> strict Subspace of a₁ means :Def3: :: RUSUB_5:def 3
the carrier of a₃ = { b₁ where B is VECTOR of a₁ : for b₁ being VECTOR of a₁ st b₂ in a₂ holds
b₂,b₁ are_orthogonal } ;
existence

proof end;

uniqueness by RUSUB_1:24;

end;

:: deftheorem Def3 defines Ort_Comp RUSUB_5:def 3 :

definition

let c₁ be RealUnitarySpace;
let c₂ be non empty Subset of c₁;
func Ort_Comp c₂ -> strict Subspace of a₁ means :Def4: :: RUSUB_5:def 4
the carrier of a₃ = { b₁ where B is VECTOR of a₁ : for b₁ being VECTOR of a₁ st b₂ in a₂ holds
b₂,b₁ are_orthogonal } ;
existence

proof end;

uniqueness by RUSUB_1:24;

end;

:: deftheorem Def4 defines Ort_Comp RUSUB_5:def 4 :

theorem Th21: :: RUSUB_5:21

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds 0. b₁ in Ort_Comp b₂

proof end;

theorem Th22: :: RUSUB_5:22

for b₁ being RealUnitarySpace holds Ort_Comp ((0). b₁) = (Omega). b₁

proof end;

theorem Th23: :: RUSUB_5:23

for b₁ being RealUnitarySpace holds Ort_Comp ((Omega). b₁) = (0). b₁

proof end;

theorem Th24: :: RUSUB_5:24

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ st b₃ <> 0. b₁ & b₃ in b₂ holds
not b₃ in Ort_Comp b₂

proof end;

theorem Th25: :: RUSUB_5:25

for b₁ being RealUnitarySpace
for b₂ being non empty Subset of b₁ holds b₂ c= the carrier of (Ort_Comp (Ort_Comp b₂))

proof end;

theorem Th26: :: RUSUB_5:26

for b₁ being RealUnitarySpace
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ holds
the carrier of (Ort_Comp b₃) c= the carrier of (Ort_Comp b₂)

proof end;

theorem Th27: :: RUSUB_5:27

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being non empty Subset of b₁ st b₃ = the carrier of b₂ holds
Ort_Comp b₃ = Ort_Comp b₂

proof end;

theorem Th28: :: RUSUB_5:28

for b₁ being RealUnitarySpace
for b₂ being non empty Subset of b₁ holds Ort_Comp b₂ = Ort_Comp (Ort_Comp (Ort_Comp b₂))

proof end;

theorem Th29: :: RUSUB_5:29

for b₁ being RealUnitarySpace
for b₂, b₃ being VECTOR of b₁ holds
( ||.(b₂ + b₃).|| ^2 = ((||.b₂.|| ^2 ) + (2 * (b₂ .|. b₃))) + (||.b₃.|| ^2 ) & ||.(b₂ - b₃).|| ^2 = ((||.b₂.|| ^2 ) - (2 * (b₂ .|. b₃))) + (||.b₃.|| ^2 ) )

proof end;

theorem Th30: :: RUSUB_5:30

for b₁ being RealUnitarySpace
for b₂, b₃ being VECTOR of b₁ st b₂,b₃ are_orthogonal holds
||.(b₂ + b₃).|| ^2 = (||.b₂.|| ^2 ) + (||.b₃.|| ^2 )

proof end;

theorem Th31: :: RUSUB_5:31

for b₁ being RealUnitarySpace
for b₂, b₃ being VECTOR of b₁ holds (||.(b₂ + b₃).|| ^2 ) + (||.(b₂ - b₃).|| ^2 ) = (2 * (||.b₂.|| ^2 )) + (2 * (||.b₃.|| ^2 ))

proof end;

theorem Th32: :: RUSUB_5:32

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁ ex b₃ being Subspace of b₁ st the carrier of b₃ = { b₄ where B is VECTOR of b₁ : b₄ .|. b₂ = 0 }

proof end;

definition

let c₁ be RealUnitarySpace;
func Family_open_set c₁ -> Subset-Family of a₁ means :Def5: :: RUSUB_5:def 5
for b₁ being Subset of a₁ holds
( b₁ in a₂ iff for b₂ being Point of a₁ st b₂ in b₁ holds
ex b₃ being Real st
( b₃ > 0 & Ball b₂,b₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Family_open_set RUSUB_5:def 5 :

theorem Th33: :: RUSUB_5:33

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

proof end;

theorem Th34: :: RUSUB_5:34

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ ex b₃ being Real st
( b₃ > 0 & Ball b₂,b₃ c= the carrier of b₁ )

proof end;

theorem Th35: :: RUSUB_5:35

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₃ in Ball b₂,b₄ holds
ex b₅ being Real st
( b₅ > 0 & Ball b₃,b₅ c= Ball b₂,b₄ )

proof end;

theorem Th36: :: RUSUB_5:36

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁
for b₅, b₆ being Real st b₃ in (Ball b₂,b₅) /\ (Ball b₄,b₆) holds
ex b₇ being Real st
( Ball b₃,b₇ c= Ball b₂,b₅ & Ball b₃,b₇ c= Ball b₄,b₆ )

proof end;

theorem Th37: :: RUSUB_5:37

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds Ball b₂,b₃ in Family_open_set b₁

proof end;

theorem Th38: :: RUSUB_5:38

for b₁ being RealUnitarySpace holds the carrier of b₁ in Family_open_set b₁

proof end;

theorem Th39: :: RUSUB_5:39

for b₁ being RealUnitarySpace
for b₂, b₃ being Subset of b₁ st b₂ in Family_open_set b₁ & b₃ in Family_open_set b₁ holds
b₂ /\ b₃ in Family_open_set b₁

proof end;

theorem Th40: :: RUSUB_5:40

for b₁ being RealUnitarySpace
for b₂ being Subset-Family of b₁ st b₂ c= Family_open_set b₁ holds
union b₂ in Family_open_set b₁

proof end;

theorem Th41: :: RUSUB_5:41

for b₁ being RealUnitarySpace holds TopStruct(# the carrier of b₁,(Family_open_set b₁) #) is TopSpace

proof end;

definition

let c₁ be RealUnitarySpace;
func TopUnitSpace c₁ -> TopStruct equals :: RUSUB_5:def 6
TopStruct(# the carrier of a₁,(Family_open_set a₁) #);
coherence ;

end;

:: deftheorem Def6 defines TopUnitSpace RUSUB_5:def 6 :

registration

let c₁ be RealUnitarySpace;
cluster TopUnitSpace a₁ -> TopSpace-like ;
coherence by Th41;

end;

registration

let c₁ be RealUnitarySpace;
cluster TopUnitSpace a₁ -> non empty TopSpace-like ;
coherence ;

end;

theorem Th42: :: RUSUB_5:42

for b₁ being RealUnitarySpace
for b₂ being Subset of (TopUnitSpace b₁) st b₂ = [#] b₁ holds
( b₂ is open & b₂ is closed )

proof end;

theorem Th43: :: RUSUB_5:43

for b₁ being RealUnitarySpace
for b₂ being Subset of (TopUnitSpace b₁) st b₂ = {} b₁ holds
( b₂ is open & b₂ is closed )

proof end;

theorem Th44: :: RUSUB_5:44

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃ being Real st the carrier of b₁ = {(0. b₁)} & b₃ <> 0 holds
Sphere b₂,b₃ is empty

proof end;

theorem Th45: :: RUSUB_5:45

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃ being Real st the carrier of b₁ <> {(0. b₁)} & b₃ > 0 holds
not Sphere b₂,b₃ is empty

proof end;

theorem Th46: :: RUSUB_5:46

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃ being Real st b₃ = 0 holds
Ball b₂,b₃ is empty

proof end;

theorem Th47: :: RUSUB_5:47

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃ being Real st the carrier of b₁ = {(0. b₁)} & b₃ > 0 holds
Ball b₂,b₃ = {(0. b₁)}

proof end;

theorem Th48: :: RUSUB_5:48

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃ being Real st the carrier of b₁ <> {(0. b₁)} & b₃ > 0 holds
ex b₄ being VECTOR of b₁ st
( b₄ <> b₂ & b₄ in Ball b₂,b₃ )

proof end;

theorem Th49: :: RUSUB_5:49

for b₁ being RealUnitarySpace holds
( the carrier of b₁ = the carrier of (TopUnitSpace b₁) & the topology of (TopUnitSpace b₁) = Family_open_set b₁ ) ;

theorem Th50: :: RUSUB_5:50

for b₁ being RealUnitarySpace
for b₂ being Subset of (TopUnitSpace b₁)
for b₃ being Real
for b₄ being Point of b₁ st b₂ = Ball b₄,b₃ holds
b₂ is open

proof end;

theorem Th51: :: RUSUB_5:51

for b₁ being RealUnitarySpace
for b₂ being Subset of (TopUnitSpace b₁) holds
( b₂ is open iff for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Real st
( b₄ > 0 & Ball b₃,b₄ c= b₂ ) )

proof end;

theorem Th52: :: RUSUB_5:52

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Real ex b₆ being Point of b₁ex b₇ being Real st (Ball b₂,b₄) \/ (Ball b₃,b₅) c= Ball b₆,b₇

proof end;

theorem Th53: :: RUSUB_5:53

for b₁ being RealUnitarySpace
for b₂ being Subset of (TopUnitSpace b₁)
for b₃ being VECTOR of b₁
for b₄ being Real st b₂ = cl_Ball b₃,b₄ holds
b₂ is closed

proof end;

theorem Th54: :: RUSUB_5:54

for b₁ being RealUnitarySpace
for b₂ being Subset of (TopUnitSpace b₁)
for b₃ being VECTOR of b₁
for b₄ being Real st b₂ = Sphere b₃,b₄ holds
b₂ is closed

proof end;