:: PSCOMP_1 semantic presentation

notation

let c₁ be set ;
synonym without_zero c₁ for with_non-empty_elements c₁;
antonym with_zero c₁ for with_non-empty_elements c₁;

end;

definition

let c₁ be set ;
redefine attr a₁ is with_non-empty_elements means :Def1: :: PSCOMP_1:def 1
not 0 in a₁;
compatibility by SETFAM_1:def 9;

end;

:: deftheorem Def1 defines without_zero PSCOMP_1:def 1 :

registration

cluster REAL -> with_zero ;
coherence by Def1;
cluster NAT -> with_zero ;
coherence by Def1;

end;

registration

cluster non empty without_zero set ;
existence

proof end;

cluster non empty with_zero set ;
existence by Def1;

end;

registration

cluster non empty without_zero Element of K40(REAL );
existence

proof end;

cluster non empty with_zero Element of K40(REAL );
existence by Def1;

end;

theorem Th1: :: PSCOMP_1:1

for b₁ being set st not b₁ is empty & b₁ is without_zero & b₁ is c=-linear holds
b₁ is centered

proof end;

registration

let c₁ be set ;
cluster non empty c=-linear with_non-empty_elements -> centered Element of K40(K40(a₁));
coherence by Th1;

end;

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
redefine func rng as rng c₃ -> Subset of a₂;
coherence by RELSET_1:12;

end;

registration

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
cluster a₃ .: a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
func " c₃ -> Function of bool a₂, bool a₁ means :Def2: :: PSCOMP_1:def 2
for b₁ being Subset of a₂ holds a₄ . b₁ = a₃ " b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines " PSCOMP_1:def 2 :

theorem Th2: :: PSCOMP_1:2

for b₁, b₂, b₃ being set
for b₄ being Subset-Family of b₂
for b₅ being Function of b₁,b₂ st b₃ in meet ((" b₅) .: b₄) holds
b₅ . b₃ in meet b₄

proof end;

theorem Th3: :: PSCOMP_1:3

for b₁, b₂ being real number st (abs b₁) + (abs b₂) = 0 holds
b₁ = 0

proof end;

theorem Th4: :: PSCOMP_1:4

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
abs b₂ < (abs b₁) + (abs b₃)

proof end;

theorem Th5: :: PSCOMP_1:5

canceled;

theorem Th6: :: PSCOMP_1:6

for b₁ being Real_Sequence st b₁ is convergent & b₁ is_not_0 & lim b₁ = 0 holds
not b₁ " is bounded

proof end;

theorem Th7: :: PSCOMP_1:7

for b₁ being Real_Sequence holds
( rng b₁ is bounded iff b₁ is bounded )

proof end;

notation

let c₁ be real-membered set ;
synonym sup c₁ for upper_bound c₁;
synonym inf c₁ for lower_bound c₁;

end;

definition

let c₁ be Subset of REAL ;
redefine func sup as sup c₁ -> Element of REAL ;
coherence by XREAL_0:def 1;
redefine func inf as inf c₁ -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

definition

let c₁ be real-membered set ;
attr a₁ is with_max means :Def3: :: PSCOMP_1:def 3
( a₁ is bounded_above & sup a₁ in a₁ );
attr a₁ is with_min means :Def4: :: PSCOMP_1:def 4
( a₁ is bounded_below & inf a₁ in a₁ );

end;

:: deftheorem Def3 defines with_max PSCOMP_1:def 3 :

:: deftheorem Def4 defines with_min PSCOMP_1:def 4 :

registration

cluster non empty bounded closed Element of K40(REAL );
existence

proof end;

end;

definition

let c₁ be Subset-Family of REAL ;
attr a₁ is open means :Def5: :: PSCOMP_1:def 5
for b₁ being Subset of REAL st b₁ in a₁ holds
b₁ is open;
attr a₁ is closed means :Def6: :: PSCOMP_1:def 6
for b₁ being Subset of REAL st b₁ in a₁ holds
b₁ is closed;

end;

:: deftheorem Def5 defines open PSCOMP_1:def 5 :

:: deftheorem Def6 defines closed PSCOMP_1:def 6 :

definition

let c₁ be Subset of REAL ;
func - c₁ -> Subset of REAL equals :: PSCOMP_1:def 7
{ (- b₁) where B is Real : b₁ in a₁ } ;
coherence

proof end;

involutiveness

proof end;

end;

:: deftheorem Def7 defines - PSCOMP_1:def 7 :

theorem Th8: :: PSCOMP_1:8

canceled;

theorem Th9: :: PSCOMP_1:9

canceled;

theorem Th10: :: PSCOMP_1:10

canceled;

theorem Th11: :: PSCOMP_1:11

canceled;

theorem Th12: :: PSCOMP_1:12

canceled;

theorem Th13: :: PSCOMP_1:13

canceled;

theorem Th14: :: PSCOMP_1:14

for b₁ being real number
for b₂ being Subset of REAL holds
( b₁ in b₂ iff - b₁ in - b₂ )

proof end;

registration

let c₁ be non empty Subset of REAL ;
cluster - a₁ -> non empty ;
coherence

proof end;

end;

Lemma14: for b₁ being Subset of REAL st b₁ is bounded_above holds
- b₁ is bounded_below

proof end;

Lemma15: for b₁ being Subset of REAL st b₁ is bounded_below holds
- b₁ is bounded_above

proof end;

theorem Th15: :: PSCOMP_1:15

for b₁ being Subset of REAL holds
( b₁ is bounded_above iff - b₁ is bounded_below )

proof end;

theorem Th16: :: PSCOMP_1:16

for b₁ being Subset of REAL holds
( b₁ is bounded_below iff - b₁ is bounded_above )

proof end;

theorem Th17: :: PSCOMP_1:17

for b₁ being non empty Subset of REAL st b₁ is bounded_below holds
inf b₁ = - (sup (- b₁))

proof end;

theorem Th18: :: PSCOMP_1:18

for b₁ being non empty Subset of REAL st b₁ is bounded_above holds
sup b₁ = - (inf (- b₁))

proof end;

Lemma19: for b₁ being Subset of REAL st b₁ is closed holds
- b₁ is closed

proof end;

theorem Th19: :: PSCOMP_1:19

for b₁ being Subset of REAL holds
( b₁ is closed iff - b₁ is closed )

proof end;

definition

let c₁ be Subset of REAL ;
let c₂ be Real;
redefine func c₂ + c₁ -> Element of K40(K311()) equals :: PSCOMP_1:def 8
{ (a₂ + b₁) where B is Real : b₁ in a₁ } ;
compatibility

proof end;

end;

:: deftheorem Def8 defines + PSCOMP_1:def 8 :

theorem Th20: :: PSCOMP_1:20

for b₁ being real number
for b₂ being Subset of REAL
for b₃ being Real holds
( b₁ in b₂ iff b₃ + b₁ in b₃ + b₂ )

proof end;

registration

let c₁ be non empty Subset of REAL ;
let c₂ be Real;
cluster a₂ + a₁ -> non empty ;
coherence

proof end;

end;

theorem Th21: :: PSCOMP_1:21

for b₁ being Subset of REAL holds b₁ = 0 + b₁

proof end;

theorem Th22: :: PSCOMP_1:22

for b₁ being Subset of REAL
for b₂, b₃ being Real holds b₂ + (b₃ + b₁) = (b₂ + b₃) + b₁

proof end;

Lemma24: for b₁ being Subset of REAL
for b₂ being Real st b₁ is bounded_above holds
b₂ + b₁ is bounded_above

proof end;

theorem Th23: :: PSCOMP_1:23

for b₁ being Subset of REAL
for b₂ being Real holds
( b₁ is bounded_above iff b₂ + b₁ is bounded_above )

proof end;

Lemma25: for b₁ being Subset of REAL
for b₂ being Real st b₁ is bounded_below holds
b₂ + b₁ is bounded_below

proof end;

theorem Th24: :: PSCOMP_1:24

for b₁ being Subset of REAL
for b₂ being Real holds
( b₁ is bounded_below iff b₂ + b₁ is bounded_below )

proof end;

theorem Th25: :: PSCOMP_1:25

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_below holds
inf (b₁ + b₂) = b₁ + (inf b₂)

proof end;

theorem Th26: :: PSCOMP_1:26

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_above holds
sup (b₁ + b₂) = b₁ + (sup b₂)

proof end;

Lemma26: for b₁ being Real
for b₂ being Subset of REAL st b₂ is closed holds
b₁ + b₂ is closed

proof end;

theorem Th27: :: PSCOMP_1:27

for b₁ being Subset of REAL
for b₂ being Real holds
( b₁ is closed iff b₂ + b₁ is closed )

proof end;

definition

let c₁ be Subset of REAL ;
func Inv c₁ -> Subset of REAL equals :: PSCOMP_1:def 9
{ (1 / b₁) where B is Real : b₁ in a₁ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Inv PSCOMP_1:def 9 :

theorem Th28: :: PSCOMP_1:28

for b₁ being real number
for b₂ being without_zero Subset of REAL holds
( b₁ in b₂ iff 1 / b₁ in Inv b₂ )

proof end;

registration

let c₁ be non empty without_zero Subset of REAL ;
cluster Inv a₁ -> non empty without_zero ;
coherence

proof end;

end;

registration

let c₁ be without_zero Subset of REAL ;
cluster Inv a₁ -> without_zero ;
coherence

proof end;

end;

theorem Th29: :: PSCOMP_1:29

for b₁ being without_zero Subset of REAL holds Inv (Inv b₁) = b₁

proof end;

theorem Th30: :: PSCOMP_1:30

for b₁ being without_zero Subset of REAL st b₁ is closed & b₁ is bounded holds
Inv b₁ is closed

proof end;

theorem Th31: :: PSCOMP_1:31

for b₁ being Subset-Family of REAL st b₁ is closed holds
meet b₁ is closed

proof end;

definition

let c₁ be Subset of REAL ;
func Cl c₁ -> Subset of REAL equals :: PSCOMP_1:def 10
meet { b₁ where B is Subset of REAL : ( a₁ c= b₁ & b₁ is closed ) } ;
coherence

proof end;

projectivity

proof end;

end;

:: deftheorem Def10 defines Cl PSCOMP_1:def 10 :

registration

let c₁ be Subset of REAL ;
cluster Cl a₁ -> closed ;
coherence

proof end;

end;

theorem Th32: :: PSCOMP_1:32

for b₁ being Subset of REAL
for b₂ being closed Subset of REAL st b₁ c= b₂ holds
Cl b₁ c= b₂

proof end;

theorem Th33: :: PSCOMP_1:33

for b₁ being Subset of REAL holds b₁ c= Cl b₁

proof end;

theorem Th34: :: PSCOMP_1:34

for b₁ being Subset of REAL holds
( b₁ is closed iff b₁ = Cl b₁ )

proof end;

theorem Th35: :: PSCOMP_1:35

Cl ({} REAL ) = {} by Th34, FCONT_3:3;

theorem Th36: :: PSCOMP_1:36

Cl ([#] REAL ) = REAL

proof end;

theorem Th37: :: PSCOMP_1:37

for b₁, b₂ being Subset of REAL st b₁ c= b₂ holds
Cl b₁ c= Cl b₂

proof end;

theorem Th38: :: PSCOMP_1:38

for b₁ being Subset of REAL
for b₂ being Real holds
( b₂ in Cl b₁ iff for b₃ being open Subset of REAL st b₂ in b₃ holds
not b₃ /\ b₁ is empty )

proof end;

theorem Th39: :: PSCOMP_1:39

for b₁ being Subset of REAL
for b₂ being Real st b₂ in Cl b₁ holds
ex b₃ being Real_Sequence st
( rng b₃ c= b₁ & b₃ is convergent & lim b₃ = b₂ )

proof end;

definition

let c₁ be set ;
let c₂ be Function of c₁, REAL ;
redefine attr bounded_below as a₂ is bounded_below means :Def11: :: PSCOMP_1:def 11
a₂ .: a₁ is bounded_below;
compatibility

proof end;

redefine attr bounded_above as a₂ is bounded_above means :Def12: :: PSCOMP_1:def 12
a₂ .: a₁ is bounded_above;
compatibility

proof end;

end;

:: deftheorem Def11 defines bounded_below PSCOMP_1:def 11 :

:: deftheorem Def12 defines bounded_above PSCOMP_1:def 12 :

definition

let c₁ be set ;
let c₂ be Function of c₁, REAL ;
canceled;
attr a₂ is with_max means :Def14: :: PSCOMP_1:def 14
a₂ .: a₁ is with_max;
attr a₂ is with_min means :Def15: :: PSCOMP_1:def 15
a₂ .: a₁ is with_min;

end;

:: deftheorem Def13 PSCOMP_1:def 13 :

:: deftheorem Def14 defines with_max PSCOMP_1:def 14 :

:: deftheorem Def15 defines with_min PSCOMP_1:def 15 :

definition

let c₁ be set ;
let c₂ be Function of c₁, REAL ;
func - c₂ -> Function of a₁, REAL means :Def16: :: PSCOMP_1:def 16
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def16 defines - PSCOMP_1:def 16 :

theorem Th40: :: PSCOMP_1:40

for b₁, b₂ being set
for b₃ being Function of b₁, REAL holds (- b₃) .: b₂ = - (b₃ .: b₂)

proof end;

Lemma42: for b₁ being non empty set
for b₂ being Function of b₁, REAL st b₂ is with_max holds
- b₂ is with_min

proof end;

Lemma43: for b₁ being non empty set
for b₂ being Function of b₁, REAL st b₂ is with_min holds
- b₂ is with_max

proof end;

theorem Th41: :: PSCOMP_1:41

for b₁ being non empty set
for b₂ being Function of b₁, REAL holds
( b₂ is with_min iff - b₂ is with_max )

proof end;

theorem Th42: :: PSCOMP_1:42

for b₁ being non empty set
for b₂ being Function of b₁, REAL holds
( b₂ is with_max iff - b₂ is with_min )

proof end;

theorem Th43: :: PSCOMP_1:43

for b₁ being set
for b₂ being Subset of REAL
for b₃ being Function of b₁, REAL holds (- b₃) " b₂ = b₃ " (- b₂)

proof end;

definition

let c₁ be set ;
let c₂ be Real;
let c₃ be Function of c₁, REAL ;
func c₂ + c₃ -> Function of a₁, REAL means :Def17: :: PSCOMP_1:def 17
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = a₂ + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines + PSCOMP_1:def 17 :

theorem Th44: :: PSCOMP_1:44

for b₁, b₂ being set
for b₃ being Function of b₁, REAL
for b₄ being Real holds (b₄ + b₃) .: b₂ = b₄ + (b₃ .: b₂)

proof end;

theorem Th45: :: PSCOMP_1:45

for b₁ being set
for b₂ being Subset of REAL
for b₃ being Function of b₁, REAL
for b₄ being Real holds (b₄ + b₃) " b₂ = b₃ " ((- b₄) + b₂)

proof end;

definition

let c₁ be set ;
let c₂ be Function of c₁, REAL ;
func Inv c₂ -> Function of a₁, REAL means :Def18: :: PSCOMP_1:def 18
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = 1 / (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def18 defines Inv PSCOMP_1:def 18 :

theorem Th46: :: PSCOMP_1:46

for b₁ being set
for b₂ being without_zero Subset of REAL
for b₃ being Function of b₁, REAL holds (Inv b₃) " b₂ = b₃ " (Inv b₂)

proof end;

definition

let c₁ be 1-sorted ;
mode RealMap of a₁ is Function of the carrier of a₁, REAL ;

end;

registration

let c₁ be non empty 1-sorted ;
cluster bounded M5(the carrier of a₁, REAL );
existence

proof end;

end;

scheme :: PSCOMP_1:sch 1
s1{ F₁() -> non empty TopStruct , P₁[ set , set ] } :

ex b₁ being RealMap of F₁() st
for b₂ being Element of F₁() holds P₁[b₂,b₁ . b₂]

provided

E50: for b₁ being set st b₁ in the carrier of F₁() holds
ex b₂ being Real st P₁[b₁,b₂]

proof end;

definition

let c₁ be 1-sorted ;
let c₂ be RealMap of c₁;
let c₃ be set ;
redefine func " as c₂ " c₃ -> Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be RealMap of c₁;
canceled;
func inf c₂ -> Real equals :Def20: :: PSCOMP_1:def 20
inf (a₂ .: the carrier of a₁);
coherence ;
func sup c₂ -> Real equals :Def21: :: PSCOMP_1:def 21
sup (a₂ .: the carrier of a₁);
coherence ;

end;

:: deftheorem Def19 PSCOMP_1:def 19 :

:: deftheorem Def20 defines inf PSCOMP_1:def 20 :

:: deftheorem Def21 defines sup PSCOMP_1:def 21 :

theorem Th47: :: PSCOMP_1:47

for b₁ being non empty TopSpace
for b₂ being V53 RealMap of b₁
for b₃ being Point of b₁ holds b₂ . b₃ >= inf b₂

proof end;

theorem Th48: :: PSCOMP_1:48

for b₁ being non empty TopSpace
for b₂ being V53 RealMap of b₁
for b₃ being Real st ( for b₄ being Point of b₁ holds b₂ . b₄ >= b₃ ) holds
inf b₂ >= b₃

proof end;

theorem Th49: :: PSCOMP_1:49

for b₁ being real number
for b₂ being non empty TopSpace
for b₃ being RealMap of b₂ st ( for b₄ being Point of b₂ holds b₃ . b₄ >= b₁ ) & ( for b₄ being real number st ( for b₅ being Point of b₂ holds b₃ . b₅ >= b₄ ) holds
b₁ >= b₄ ) holds
b₁ = inf b₃

proof end;

theorem Th50: :: PSCOMP_1:50

for b₁ being non empty TopSpace
for b₂ being V52 RealMap of b₁
for b₃ being Point of b₁ holds b₂ . b₃ <= sup b₂

proof end;

theorem Th51: :: PSCOMP_1:51

for b₁ being non empty TopSpace
for b₂ being V52 RealMap of b₁
for b₃ being real number st ( for b₄ being Point of b₁ holds b₂ . b₄ <= b₃ ) holds
sup b₂ <= b₃

proof end;

theorem Th52: :: PSCOMP_1:52

for b₁ being real number
for b₂ being non empty TopSpace
for b₃ being RealMap of b₂ st ( for b₄ being Point of b₂ holds b₃ . b₄ <= b₁ ) & ( for b₄ being real number st ( for b₅ being Point of b₂ holds b₃ . b₅ <= b₄ ) holds
b₁ <= b₄ ) holds
b₁ = sup b₃

proof end;

theorem Th53: :: PSCOMP_1:53

for b₁ being non empty 1-sorted
for b₂ being bounded RealMap of b₁ holds inf b₂ <= sup b₂

proof end;

definition

let c₁ be TopStruct ;
let c₂ be RealMap of c₁;
canceled;
canceled;
canceled;
attr a₂ is continuous means :Def25: :: PSCOMP_1:def 25
for b₁ being Subset of REAL st b₁ is closed holds
a₂ " b₁ is closed;

end;

:: deftheorem Def22 PSCOMP_1:def 22 :

:: deftheorem Def23 PSCOMP_1:def 23 :

:: deftheorem Def24 PSCOMP_1:def 24 :

:: deftheorem Def25 defines continuous PSCOMP_1:def 25 :

registration

let c₁ be non empty TopSpace;
cluster continuous M5(the carrier of a₁, REAL );
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
cluster continuous M5(the carrier of a₂, REAL );
existence

proof end;

end;

theorem Th54: :: PSCOMP_1:54

for b₁ being TopStruct
for b₂ being RealMap of b₁ holds
( b₂ is continuous iff for b₃ being Subset of REAL st b₃ is open holds
b₂ " b₃ is open )

proof end;

theorem Th55: :: PSCOMP_1:55

for b₁ being TopStruct
for b₂ being RealMap of b₁ st b₂ is continuous holds
- b₂ is continuous

proof end;

theorem Th56: :: PSCOMP_1:56

for b₁ being Real
for b₂ being TopStruct
for b₃ being RealMap of b₂ st b₃ is continuous holds
b₁ + b₃ is continuous

proof end;

theorem Th57: :: PSCOMP_1:57

for b₁ being TopStruct
for b₂ being RealMap of b₁ st b₂ is continuous & not 0 in rng b₂ holds
Inv b₂ is continuous

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of bool c₁, bool c₂;
let c₄ be Subset-Family of c₁;
redefine func .: as c₃ .: c₄ -> Subset-Family of a₂;
coherence

proof end;

end;

theorem Th58: :: PSCOMP_1:58

for b₁ being TopStruct
for b₂ being RealMap of b₁
for b₃ being Subset-Family of REAL st b₂ is continuous & b₃ is open holds
(" b₂) .: b₃ is open

proof end;

theorem Th59: :: PSCOMP_1:59

for b₁ being TopStruct
for b₂ being RealMap of b₁
for b₃ being Subset-Family of REAL st b₂ is continuous & b₃ is closed holds
(" b₂) .: b₃ is closed

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Subset of c₁;
let c₃ be RealMap of c₁;
func c₃ || c₂ -> RealMap of (a₁ | a₂) equals :: PSCOMP_1:def 26
a₃ | a₂;
coherence

proof end;

end;

:: deftheorem Def26 defines || PSCOMP_1:def 26 :

registration

let c₁ be non empty TopSpace;
cluster non empty compact Element of K40(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be continuous RealMap of c₁;
let c₃ be Subset of c₁;
cluster a₂ || a₃ -> continuous ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty compact Subset of c₁;
cluster a₁ | a₂ -> compact ;
coherence by COMPTS_1:12;

end;

theorem Th60: :: PSCOMP_1:60

for b₁ being non empty TopSpace holds
( ( for b₂ being RealMap of b₁ st b₂ is continuous holds
b₂ is with_max ) iff for b₂ being RealMap of b₁ st b₂ is continuous holds
b₂ is with_min )

proof end;

theorem Th61: :: PSCOMP_1:61

for b₁ being non empty TopSpace holds
( ( for b₂ being RealMap of b₁ st b₂ is continuous holds
b₂ is bounded ) iff for b₂ being RealMap of b₁ st b₂ is continuous holds
b₂ is with_max )

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is pseudocompact means :Def27: :: PSCOMP_1:def 27
for b₁ being RealMap of a₁ st b₁ is continuous holds
b₁ is bounded;

end;

:: deftheorem Def27 defines pseudocompact PSCOMP_1:def 27 :

registration

cluster non empty compact -> non empty pseudocompact TopStruct ;
coherence

proof end;

end;

registration

cluster non empty compact pseudocompact TopStruct ;
existence

proof end;

end;

registration

let c₁ be non empty pseudocompact TopSpace;
cluster continuous -> bounded with_max with_min M5(the carrier of a₁, REAL );
coherence

proof end;

end;

theorem Th62: :: PSCOMP_1:62

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁
for b₃ being compact Subset of b₁
for b₄ being continuous RealMap of b₁ st b₂ c= b₃ holds
inf (b₄ || b₃) <= inf (b₄ || b₂)

proof end;

theorem Th63: :: PSCOMP_1:63

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁
for b₃ being compact Subset of b₁
for b₄ being continuous RealMap of b₁ st b₂ c= b₃ holds
sup (b₄ || b₂) <= sup (b₄ || b₃)

proof end;

theorem Th64: :: PSCOMP_1:64

for b₁ being Nat
for b₂, b₃ being compact Subset of (TOP-REAL b₁) holds b₂ /\ b₃ is compact

proof end;

definition

func proj1 -> RealMap of (TOP-REAL 2) means :Def28: :: PSCOMP_1:def 28
for b₁ being Point of (TOP-REAL 2) holds a₁ . b₁ = b₁ `1 ;
existence

proof end;

uniqueness

proof end;

func proj2 -> RealMap of (TOP-REAL 2) means :Def29: :: PSCOMP_1:def 29
for b₁ being Point of (TOP-REAL 2) holds a₁ . b₁ = b₁ `2 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines proj1 PSCOMP_1:def 28 :

:: deftheorem Def29 defines proj2 PSCOMP_1:def 29 :

theorem Th65: :: PSCOMP_1:65

for b₁, b₂ being real number holds proj1 " ].b₁,b₂.[ = { |[b₃,b₄]| where B is Real, B is Real : ( b₁ < b₃ & b₃ < b₂ ) }

proof end;

theorem Th66: :: PSCOMP_1:66

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃ being Real st b₁ = { |[b₄,b₅]| where B is Real, B is Real : ( b₂ < b₄ & b₄ < b₃ ) } holds
b₁ is open

proof end;

theorem Th67: :: PSCOMP_1:67

for b₁, b₂ being real number holds proj2 " ].b₁,b₂.[ = { |[b₃,b₄]| where B is Real, B is Real : ( b₁ < b₄ & b₄ < b₂ ) }

proof end;

theorem Th68: :: PSCOMP_1:68

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃ being Real st b₁ = { |[b₄,b₅]| where B is Real, B is Real : ( b₂ < b₅ & b₅ < b₃ ) } holds
b₁ is open

proof end;

registration

cluster proj1 -> continuous ;
coherence

proof end;

cluster proj2 -> continuous ;
coherence

proof end;

end;

theorem Th69: :: PSCOMP_1:69

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ holds
(proj1 || b₁) . b₂ = b₂ `1

proof end;

theorem Th70: :: PSCOMP_1:70

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ holds
(proj2 || b₁) . b₂ = b₂ `2

proof end;

Lemma75: for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty compact Subset of (TOP-REAL 2) st b₁ in b₂ holds
( inf (proj1 || b₂) <= b₁ `1 & b₁ `1 <= sup (proj1 || b₂) & inf (proj2 || b₂) <= b₁ `2 & b₁ `2 <= sup (proj2 || b₂) )

proof end;

definition

let c₁ be Subset of (TOP-REAL 2);
func W-bound c₁ -> Real equals :: PSCOMP_1:def 30
inf (proj1 || a₁);
coherence ;
func N-bound c₁ -> Real equals :Def31: :: PSCOMP_1:def 31
sup (proj2 || a₁);
coherence ;
func E-bound c₁ -> Real equals :Def32: :: PSCOMP_1:def 32
sup (proj1 || a₁);
coherence ;
func S-bound c₁ -> Real equals :: PSCOMP_1:def 33
inf (proj2 || a₁);
coherence ;

end;

:: deftheorem Def30 defines W-bound PSCOMP_1:def 30 :

:: deftheorem Def31 defines N-bound PSCOMP_1:def 31 :

:: deftheorem Def32 defines E-bound PSCOMP_1:def 32 :

:: deftheorem Def33 defines S-bound PSCOMP_1:def 33 :

theorem Th71: :: PSCOMP_1:71

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty compact Subset of (TOP-REAL 2) st b₁ in b₂ holds
( W-bound b₂ <= b₁ `1 & b₁ `1 <= E-bound b₂ & S-bound b₂ <= b₁ `2 & b₁ `2 <= N-bound b₂ ) by Lemma75;

definition

let c₁ be Subset of (TOP-REAL 2);
func SW-corner c₁ -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 34
|[(W-bound a₁),(S-bound a₁)]|;
coherence ;
func NW-corner c₁ -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 35
|[(W-bound a₁),(N-bound a₁)]|;
coherence ;
func NE-corner c₁ -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 36
|[(E-bound a₁),(N-bound a₁)]|;
coherence ;
func SE-corner c₁ -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 37
|[(E-bound a₁),(S-bound a₁)]|;
coherence ;

end;

:: deftheorem Def34 defines SW-corner PSCOMP_1:def 34 :

:: deftheorem Def35 defines NW-corner PSCOMP_1:def 35 :

:: deftheorem Def36 defines NE-corner PSCOMP_1:def 36 :

:: deftheorem Def37 defines SE-corner PSCOMP_1:def 37 :

theorem Th72: :: PSCOMP_1:72

for b₁ being Subset of (TOP-REAL 2) holds (SW-corner b₁) `1 = W-bound b₁ by EUCLID:56;

theorem Th73: :: PSCOMP_1:73

for b₁ being Subset of (TOP-REAL 2) holds (SW-corner b₁) `2 = S-bound b₁ by EUCLID:56;

theorem Th74: :: PSCOMP_1:74

for b₁ being Subset of (TOP-REAL 2) holds (NW-corner b₁) `1 = W-bound b₁ by EUCLID:56;

theorem Th75: :: PSCOMP_1:75

for b₁ being Subset of (TOP-REAL 2) holds (NW-corner b₁) `2 = N-bound b₁ by EUCLID:56;

theorem Th76: :: PSCOMP_1:76

for b₁ being Subset of (TOP-REAL 2) holds (NE-corner b₁) `1 = E-bound b₁ by EUCLID:56;

theorem Th77: :: PSCOMP_1:77

for b₁ being Subset of (TOP-REAL 2) holds (NE-corner b₁) `2 = N-bound b₁ by EUCLID:56;

theorem Th78: :: PSCOMP_1:78

for b₁ being Subset of (TOP-REAL 2) holds (SE-corner b₁) `1 = E-bound b₁ by EUCLID:56;

theorem Th79: :: PSCOMP_1:79

for b₁ being Subset of (TOP-REAL 2) holds (SE-corner b₁) `2 = S-bound b₁ by EUCLID:56;

theorem Th80: :: PSCOMP_1:80

for b₁ being Subset of (TOP-REAL 2) holds (SW-corner b₁) `1 = (NW-corner b₁) `1

proof end;

theorem Th81: :: PSCOMP_1:81

for b₁ being Subset of (TOP-REAL 2) holds (SE-corner b₁) `1 = (NE-corner b₁) `1

proof end;

theorem Th82: :: PSCOMP_1:82

for b₁ being Subset of (TOP-REAL 2) holds (NW-corner b₁) `2 = (NE-corner b₁) `2

proof end;

theorem Th83: :: PSCOMP_1:83

for b₁ being Subset of (TOP-REAL 2) holds (SW-corner b₁) `2 = (SE-corner b₁) `2

proof end;

definition

let c₁ be Subset of (TOP-REAL 2);
func W-most c₁ -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 38
(LSeg (SW-corner a₁),(NW-corner a₁)) /\ a₁;
coherence ;
func N-most c₁ -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 39
(LSeg (NW-corner a₁),(NE-corner a₁)) /\ a₁;
coherence ;
func E-most c₁ -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 40
(LSeg (SE-corner a₁),(NE-corner a₁)) /\ a₁;
coherence ;
func S-most c₁ -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 41
(LSeg (SW-corner a₁),(SE-corner a₁)) /\ a₁;
coherence ;

end;

:: deftheorem Def38 defines W-most PSCOMP_1:def 38 :

:: deftheorem Def39 defines N-most PSCOMP_1:def 39 :

:: deftheorem Def40 defines E-most PSCOMP_1:def 40 :

:: deftheorem Def41 defines S-most PSCOMP_1:def 41 :

registration

let c₁ be non empty compact Subset of (TOP-REAL 2);
cluster W-most a₁ -> non empty compact ;
coherence

proof end;

cluster N-most a₁ -> non empty compact ;
coherence

proof end;

cluster E-most a₁ -> non empty compact ;
coherence

proof end;

cluster S-most a₁ -> non empty compact ;
coherence

proof end;

end;

definition

end;

:: deftheorem Def42 defines W-min PSCOMP_1:def 42 :

:: deftheorem Def43 defines W-max PSCOMP_1:def 43 :

:: deftheorem Def44 defines N-min PSCOMP_1:def 44 :

:: deftheorem Def45 defines N-max PSCOMP_1:def 45 :

:: deftheorem Def46 defines E-max PSCOMP_1:def 46 :

:: deftheorem Def47 defines E-min PSCOMP_1:def 47 :

:: deftheorem Def48 defines S-max PSCOMP_1:def 48 :

:: deftheorem Def49 defines S-min PSCOMP_1:def 49 :

theorem Th84: :: PSCOMP_1:84

for b₁ being Subset of (TOP-REAL 2) holds
( (W-min b₁) `1 = W-bound b₁ & (W-max b₁) `1 = W-bound b₁ ) by EUCLID:56;

theorem Th85: :: PSCOMP_1:85

for b₁ being Subset of (TOP-REAL 2) holds
( (SW-corner b₁) `1 = (W-min b₁) `1 & (SW-corner b₁) `1 = (W-max b₁) `1 & (W-min b₁) `1 = (W-max b₁) `1 & (W-min b₁) `1 = (NW-corner b₁) `1 & (W-max b₁) `1 = (NW-corner b₁) `1 )

proof end;

theorem Th86: :: PSCOMP_1:86

for b₁ being Subset of (TOP-REAL 2) holds
( (W-min b₁) `2 = inf (proj2 || (W-most b₁)) & (W-max b₁) `2 = sup (proj2 || (W-most b₁)) ) by EUCLID:56;

theorem Th87: :: PSCOMP_1:87

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (SW-corner b₁) `2 <= (W-min b₁) `2 & (SW-corner b₁) `2 <= (W-max b₁) `2 & (SW-corner b₁) `2 <= (NW-corner b₁) `2 & (W-min b₁) `2 <= (W-max b₁) `2 & (W-min b₁) `2 <= (NW-corner b₁) `2 & (W-max b₁) `2 <= (NW-corner b₁) `2 )

proof end;

theorem Th88: :: PSCOMP_1:88

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty Subset of (TOP-REAL 2) st b₁ in W-most b₂ holds
( b₁ `1 = (W-min b₂) `1 & ( b₂ is compact implies ( (W-min b₂) `2 <= b₁ `2 & b₁ `2 <= (W-max b₂) `2 ) ) )

proof end;

theorem Th89: :: PSCOMP_1:89

for b₁ being non empty compact Subset of (TOP-REAL 2) holds W-most b₁ c= LSeg (W-min b₁),(W-max b₁)

proof end;

theorem Th90: :: PSCOMP_1:90

for b₁ being non empty compact Subset of (TOP-REAL 2) holds LSeg (W-min b₁),(W-max b₁) c= LSeg (SW-corner b₁),(NW-corner b₁)

proof end;

theorem Th91: :: PSCOMP_1:91

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( W-min b₁ in W-most b₁ & W-max b₁ in W-most b₁ )

proof end;

theorem Th92: :: PSCOMP_1:92

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SW-corner b₁),(W-min b₁)) /\ b₁ = {(W-min b₁)} & (LSeg (W-max b₁),(NW-corner b₁)) /\ b₁ = {(W-max b₁)} )

proof end;

theorem Th93: :: PSCOMP_1:93

for b₁ being non empty compact Subset of (TOP-REAL 2) st W-min b₁ = W-max b₁ holds
W-most b₁ = {(W-min b₁)}

proof end;

theorem Th94: :: PSCOMP_1:94

for b₁ being Subset of (TOP-REAL 2) holds
( (N-min b₁) `2 = N-bound b₁ & (N-max b₁) `2 = N-bound b₁ ) by EUCLID:56;

theorem Th95: :: PSCOMP_1:95

for b₁ being Subset of (TOP-REAL 2) holds
( (NW-corner b₁) `2 = (N-min b₁) `2 & (NW-corner b₁) `2 = (N-max b₁) `2 & (N-min b₁) `2 = (N-max b₁) `2 & (N-min b₁) `2 = (NE-corner b₁) `2 & (N-max b₁) `2 = (NE-corner b₁) `2 )

proof end;

theorem Th96: :: PSCOMP_1:96

for b₁ being Subset of (TOP-REAL 2) holds
( (N-min b₁) `1 = inf (proj1 || (N-most b₁)) & (N-max b₁) `1 = sup (proj1 || (N-most b₁)) ) by EUCLID:56;

theorem Th97: :: PSCOMP_1:97

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (NW-corner b₁) `1 <= (N-min b₁) `1 & (NW-corner b₁) `1 <= (N-max b₁) `1 & (NW-corner b₁) `1 <= (NE-corner b₁) `1 & (N-min b₁) `1 <= (N-max b₁) `1 & (N-min b₁) `1 <= (NE-corner b₁) `1 & (N-max b₁) `1 <= (NE-corner b₁) `1 )

proof end;

theorem Th98: :: PSCOMP_1:98

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty Subset of (TOP-REAL 2) st b₁ in N-most b₂ holds
( b₁ `2 = (N-min b₂) `2 & ( b₂ is compact implies ( (N-min b₂) `1 <= b₁ `1 & b₁ `1 <= (N-max b₂) `1 ) ) )

proof end;

theorem Th99: :: PSCOMP_1:99

for b₁ being non empty compact Subset of (TOP-REAL 2) holds N-most b₁ c= LSeg (N-min b₁),(N-max b₁)

proof end;

theorem Th100: :: PSCOMP_1:100

for b₁ being non empty compact Subset of (TOP-REAL 2) holds LSeg (N-min b₁),(N-max b₁) c= LSeg (NW-corner b₁),(NE-corner b₁)

proof end;

theorem Th101: :: PSCOMP_1:101

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( N-min b₁ in N-most b₁ & N-max b₁ in N-most b₁ )

proof end;

theorem Th102: :: PSCOMP_1:102

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (NW-corner b₁),(N-min b₁)) /\ b₁ = {(N-min b₁)} & (LSeg (N-max b₁),(NE-corner b₁)) /\ b₁ = {(N-max b₁)} )

proof end;

theorem Th103: :: PSCOMP_1:103

for b₁ being non empty compact Subset of (TOP-REAL 2) st N-min b₁ = N-max b₁ holds
N-most b₁ = {(N-min b₁)}

proof end;

theorem Th104: :: PSCOMP_1:104

for b₁ being Subset of (TOP-REAL 2) holds
( (E-min b₁) `1 = E-bound b₁ & (E-max b₁) `1 = E-bound b₁ ) by EUCLID:56;

theorem Th105: :: PSCOMP_1:105

for b₁ being Subset of (TOP-REAL 2) holds
( (SE-corner b₁) `1 = (E-min b₁) `1 & (SE-corner b₁) `1 = (E-max b₁) `1 & (E-min b₁) `1 = (E-max b₁) `1 & (E-min b₁) `1 = (NE-corner b₁) `1 & (E-max b₁) `1 = (NE-corner b₁) `1 )

proof end;

theorem Th106: :: PSCOMP_1:106

for b₁ being Subset of (TOP-REAL 2) holds
( (E-min b₁) `2 = inf (proj2 || (E-most b₁)) & (E-max b₁) `2 = sup (proj2 || (E-most b₁)) ) by EUCLID:56;

theorem Th107: :: PSCOMP_1:107

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (SE-corner b₁) `2 <= (E-min b₁) `2 & (SE-corner b₁) `2 <= (E-max b₁) `2 & (SE-corner b₁) `2 <= (NE-corner b₁) `2 & (E-min b₁) `2 <= (E-max b₁) `2 & (E-min b₁) `2 <= (NE-corner b₁) `2 & (E-max b₁) `2 <= (NE-corner b₁) `2 )

proof end;

theorem Th108: :: PSCOMP_1:108

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty Subset of (TOP-REAL 2) st b₁ in E-most b₂ holds
( b₁ `1 = (E-min b₂) `1 & ( b₂ is compact implies ( (E-min b₂) `2 <= b₁ `2 & b₁ `2 <= (E-max b₂) `2 ) ) )

proof end;

theorem Th109: :: PSCOMP_1:109

for b₁ being non empty compact Subset of (TOP-REAL 2) holds E-most b₁ c= LSeg (E-min b₁),(E-max b₁)

proof end;

theorem Th110: :: PSCOMP_1:110

for b₁ being non empty compact Subset of (TOP-REAL 2) holds LSeg (E-min b₁),(E-max b₁) c= LSeg (SE-corner b₁),(NE-corner b₁)

proof end;

theorem Th111: :: PSCOMP_1:111

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( E-min b₁ in E-most b₁ & E-max b₁ in E-most b₁ )

proof end;

theorem Th112: :: PSCOMP_1:112

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SE-corner b₁),(E-min b₁)) /\ b₁ = {(E-min b₁)} & (LSeg (E-max b₁),(NE-corner b₁)) /\ b₁ = {(E-max b₁)} )

proof end;

theorem Th113: :: PSCOMP_1:113

for b₁ being non empty compact Subset of (TOP-REAL 2) st E-min b₁ = E-max b₁ holds
E-most b₁ = {(E-min b₁)}

proof end;

theorem Th114: :: PSCOMP_1:114

for b₁ being Subset of (TOP-REAL 2) holds
( (S-min b₁) `2 = S-bound b₁ & (S-max b₁) `2 = S-bound b₁ ) by EUCLID:56;

theorem Th115: :: PSCOMP_1:115

for b₁ being Subset of (TOP-REAL 2) holds
( (SW-corner b₁) `2 = (S-min b₁) `2 & (SW-corner b₁) `2 = (S-max b₁) `2 & (S-min b₁) `2 = (S-max b₁) `2 & (S-min b₁) `2 = (SE-corner b₁) `2 & (S-max b₁) `2 = (SE-corner b₁) `2 )

proof end;

theorem Th116: :: PSCOMP_1:116

for b₁ being Subset of (TOP-REAL 2) holds
( (S-min b₁) `1 = inf (proj1 || (S-most b₁)) & (S-max b₁) `1 = sup (proj1 || (S-most b₁)) ) by EUCLID:56;

theorem Th117: :: PSCOMP_1:117

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (SW-corner b₁) `1 <= (S-min b₁) `1 & (SW-corner b₁) `1 <= (S-max b₁) `1 & (SW-corner b₁) `1 <= (SE-corner b₁) `1 & (S-min b₁) `1 <= (S-max b₁) `1 & (S-min b₁) `1 <= (SE-corner b₁) `1 & (S-max b₁) `1 <= (SE-corner b₁) `1 )

proof end;

theorem Th118: :: PSCOMP_1:118

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty Subset of (TOP-REAL 2) st b₁ in S-most b₂ holds
( b₁ `2 = (S-min b₂) `2 & ( b₂ is compact implies ( (S-min b₂) `1 <= b₁ `1 & b₁ `1 <= (S-max b₂) `1 ) ) )

proof end;

theorem Th119: :: PSCOMP_1:119

for b₁ being non empty compact Subset of (TOP-REAL 2) holds S-most b₁ c= LSeg (S-min b₁),(S-max b₁)

proof end;

theorem Th120: :: PSCOMP_1:120

for b₁ being non empty compact Subset of (TOP-REAL 2) holds LSeg (S-min b₁),(S-max b₁) c= LSeg (SW-corner b₁),(SE-corner b₁)

proof end;

theorem Th121: :: PSCOMP_1:121

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( S-min b₁ in S-most b₁ & S-max b₁ in S-most b₁ )

proof end;

theorem Th122: :: PSCOMP_1:122

for b₁ being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SW-corner b₁),(S-min b₁)) /\ b₁ = {(S-min b₁)} & (LSeg (S-max b₁),(SE-corner b₁)) /\ b₁ = {(S-max b₁)} )

proof end;

theorem Th123: :: PSCOMP_1:123

for b₁ being non empty compact Subset of (TOP-REAL 2) st S-min b₁ = S-max b₁ holds
S-most b₁ = {(S-min b₁)}

proof end;

theorem Th124: :: PSCOMP_1:124

for b₁ being Subset of (TOP-REAL 2) st W-max b₁ = N-min b₁ holds
W-max b₁ = NW-corner b₁

proof end;

theorem Th125: :: PSCOMP_1:125

for b₁ being Subset of (TOP-REAL 2) st N-max b₁ = E-max b₁ holds
N-max b₁ = NE-corner b₁

proof end;

theorem Th126: :: PSCOMP_1:126

for b₁ being Subset of (TOP-REAL 2) st E-min b₁ = S-max b₁ holds
E-min b₁ = SE-corner b₁

proof end;

theorem Th127: :: PSCOMP_1:127

for b₁ being Subset of (TOP-REAL 2) st S-min b₁ = W-min b₁ holds
S-min b₁ = SW-corner b₁

proof end;