:: TOPMETR semantic presentation

theorem Th1: :: TOPMETR:1

for b₁ being TopStruct
for b₂ being Subset-Family of b₁ holds
( b₂ is_a_cover_of b₁ iff the carrier of b₁ c= union b₂ )

proof end;

theorem Th2: :: TOPMETR:2

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being Point of b₂ holds b₃ is Point of b₁

proof end;

theorem Th3: :: TOPMETR:3

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ st b₁ is_T2 holds
b₂ is_T2

proof end;

theorem Th4: :: TOPMETR:4

for b₁ being TopSpace
for b₂, b₃ being SubSpace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is SubSpace of b₃

proof end;

theorem Th5: :: TOPMETR:5

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₁ | b₂ is SubSpace of b₁ | (b₂ \/ b₃) & b₁ | b₃ is SubSpace of b₁ | (b₂ \/ b₃) )

proof end;

theorem Th6: :: TOPMETR:6

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being non empty Subset of b₁ st b₂ in b₃ holds
for b₄ being a_neighborhood of b₂
for b₅ being Point of (b₁ | b₃)
for b₆ being Subset of (b₁ | b₃) st b₆ = b₄ /\ b₃ & b₅ = b₂ holds
b₆ is a_neighborhood of b₅

proof end;

theorem Th7: :: TOPMETR:7

for b₁, b₂, b₃ being TopSpace
for b₄ being Function of b₁,b₃ st b₄ is continuous & b₃ is SubSpace of b₂ holds
for b₅ being Function of b₁,b₂ st b₅ = b₄ holds
b₅ is continuous

proof end;

theorem Th8: :: TOPMETR:8

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being SubSpace of b₂ st b₃ is continuous holds
for b₅ being Function of b₁,b₄ st b₅ = b₃ holds
b₅ is continuous

proof end;

theorem Th9: :: TOPMETR:9

for b₁, b₂ being TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₂ st b₃ is continuous holds
for b₅ being Function of b₁,(b₂ | b₄) st b₅ = b₃ holds
b₅ is continuous

proof end;

theorem Th10: :: TOPMETR:10

for b₁ being TopStruct
for b₂ being non empty TopStruct
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂
for b₅ being Function of (b₁ | b₃),b₂ st b₄ is continuous & b₅ = b₄ | b₃ holds
b₅ is continuous

proof end;

Lemma4: for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being real number st b₃ > 0 holds
b₂ in Ball b₂,b₃
by TBSP_1:16;

Lemma5: for b₁ being MetrSpace holds MetrStruct(# the carrier of b₁,the distance of b₁ #) is MetrSpace

proof end;

definition

let c₁ be MetrSpace;
mode SubSpace of c₁ -> MetrSpace means :Def1: :: TOPMETR:def 1
( the carrier of a₂ c= the carrier of a₁ & ( for b₁, b₂ being Point of a₂ holds the distance of a₂ . b₁,b₂ = the distance of a₁ . b₁,b₂ ) );
existence

proof end;

end;

:: deftheorem Def1 defines SubSpace TOPMETR:def 1 :

registration

let c₁ be MetrSpace;
cluster strict SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty MetrSpace;
cluster non empty strict SubSpace of a₁;
existence

proof end;

end;

theorem Th11: :: TOPMETR:11

canceled;

theorem Th12: :: TOPMETR:12

for b₁ being non empty MetrSpace
for b₂ being non empty SubSpace of b₁
for b₃ being Point of b₂ holds b₃ is Point of b₁

proof end;

theorem Th13: :: TOPMETR:13

for b₁ being real number
for b₂ being MetrSpace
for b₃ being SubSpace of b₂
for b₄ being Point of b₂
for b₅ being Point of b₃ st b₄ = b₅ holds
Ball b₅,b₁ = (Ball b₄,b₁) /\ the carrier of b₃

proof end;

definition

let c₁ be non empty MetrSpace;
let c₂ be non empty Subset of c₁;
func c₁ | c₂ -> strict SubSpace of a₁ means :Def2: :: TOPMETR:def 2
the carrier of a₃ = a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines | TOPMETR:def 2 :

registration

let c₁ be non empty MetrSpace;
let c₂ be non empty Subset of c₁;
cluster a₁ | a₂ -> non empty strict ;
coherence

proof end;

end;

definition

let c₁, c₂ be real number ;
assume E10: c₁ <= c₂ ;
func Closed-Interval-MSpace c₁,c₂ -> non empty strict SubSpace of RealSpace means :Def3: :: TOPMETR:def 3
for b₁ being non empty Subset of RealSpace st b₁ = [.a₁,a₂.] holds
a₃ = RealSpace | b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Closed-Interval-MSpace TOPMETR:def 3 :

theorem Th14: :: TOPMETR:14

for b₁, b₂ being real number st b₁ <= b₂ holds
the carrier of (Closed-Interval-MSpace b₁,b₂) = [.b₁,b₂.]

proof end;

definition

let c₁ be MetrStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is being_ball-family means :Def4: :: TOPMETR:def 4
for b₁ being set st b₁ in a₂ holds
ex b₂ being Point of a₁ex b₃ being Real st b₁ = Ball b₂,b₃;
pred c₂ is_a_cover_of c₁ means :Def5: :: TOPMETR:def 5
the carrier of a₁ c= union a₂;

end;

:: deftheorem Def4 defines being_ball-family TOPMETR:def 4 :

:: deftheorem Def5 defines is_a_cover_of TOPMETR:def 5 :

notation

let c₁ be MetrStruct ;
let c₂ be Subset-Family of c₁;
synonym c₂ is_ball-family for being_ball-family c₂;

end;

theorem Th15: :: TOPMETR:15

for b₁, b₂ being Point of RealSpace
for b₃, b₄ being real number st b₃ = b₁ & b₄ = b₂ holds
dist b₁,b₂ = abs (b₃ - b₄)

proof end;

theorem Th16: :: TOPMETR:16

for b₁ being MetrStruct holds
( the carrier of b₁ = the carrier of (TopSpaceMetr b₁) & the topology of (TopSpaceMetr b₁) = Family_open_set b₁ )

proof end;

theorem Th17: :: TOPMETR:17

canceled;

theorem Th18: :: TOPMETR:18

canceled;

theorem Th19: :: TOPMETR:19

for b₁ being non empty MetrSpace
for b₂ being non empty SubSpace of b₁ holds TopSpaceMetr b₂ is SubSpace of TopSpaceMetr b₁

proof end;

theorem Th20: :: TOPMETR:20

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being non empty Subset of (Euclid b₁) st b₂ = b₃ holds
(TOP-REAL b₁) | b₂ = TopSpaceMetr ((Euclid b₁) | b₃)

proof end;

theorem Th21: :: TOPMETR:21

for b₁ being real number
for b₂ being triangle MetrStruct
for b₃ being Point of b₂
for b₄ being Subset of (TopSpaceMetr b₂) st b₄ = Ball b₃,b₁ holds
b₄ is open

proof end;

theorem Th22: :: TOPMETR:22

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) holds
( b₂ is open iff for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being real number st
( b₄ > 0 & Ball b₃,b₄ c= b₂ ) )

proof end;

definition

let c₁ be MetrStruct ;
attr a₁ is compact means :Def6: :: TOPMETR:def 6
TopSpaceMetr a₁ is compact;

end;

:: deftheorem Def6 defines compact TOPMETR:def 6 :

theorem Th23: :: TOPMETR:23

for b₁ being non empty MetrSpace holds
( b₁ is compact iff for b₂ being Subset-Family of b₁ st b₂ is_ball-family & b₂ is_a_cover_of b₁ holds
ex b₃ being Subset-Family of b₁ st
( b₃ c= b₂ & b₃ is_a_cover_of b₁ & b₃ is finite ) )

proof end;

definition

func R^1 -> strict TopSpace equals :: TOPMETR:def 7
TopSpaceMetr RealSpace ;
correctness ;

end;

:: deftheorem Def7 defines R^1 TOPMETR:def 7 :

registration

cluster R^1 -> non empty strict ;
coherence ;

end;

theorem Th24: :: TOPMETR:24

the carrier of R^1 = REAL

proof end;

registration

let c₁ be set ;
let c₂ be PartFunc of c₁,the carrier of R^1 ;
let c₃ be set ;
cluster a₂ . a₃ -> real ;
coherence

proof end;

end;

definition

let c₁, c₂ be real number ;
func Closed-Interval-TSpace c₁,c₂ -> non empty strict SubSpace of R^1 equals :: TOPMETR:def 8
TopSpaceMetr (Closed-Interval-MSpace a₁,a₂);
coherence by Th19;

end;

:: deftheorem Def8 defines Closed-Interval-TSpace TOPMETR:def 8 :

theorem Th25: :: TOPMETR:25

for b₁, b₂ being real number st b₁ <= b₂ holds
the carrier of (Closed-Interval-TSpace b₁,b₂) = [.b₁,b₂.]

proof end;

theorem Th26: :: TOPMETR:26

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃ being Subset of R^1 st b₃ = [.b₁,b₂.] holds
Closed-Interval-TSpace b₁,b₂ = R^1 | b₃

proof end;

theorem Th27: :: TOPMETR:27

Closed-Interval-TSpace 0,1 = I[01]

proof end;

definition

redefine func I[01] as I[01] -> strict SubSpace of R^1 ;
coherence by Th27;

end;

Lemma24: for b₁, b₂, b₃ being real number st b₃ >= 0 & b₁ + b₃ <= b₂ holds
b₁ <= b₂

proof end;

theorem Th28: :: TOPMETR:28

for b₁ being Function of R^1 ,R^1 st ex b₂, b₃ being Real st
for b₄ being Real holds b₁ . b₄ = (b₂ * b₄) + b₃ holds
b₁ is continuous

proof end;