:: BORSUK_4 semantic presentation

registration

cluster -> non trivial Element of K22(the carrier of (TOP-REAL 2));
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th1: :: BORSUK_4:1

for b₁ being non empty set
for b₂, b₃ being non empty Subset of b₁ st b₂ c< b₃ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₂ c= b₃ \ {b₄} )

proof end;

theorem Th2: :: BORSUK_4:2

for b₁ being non empty set
for b₂ being non empty Subset of b₁ holds
( b₂ is trivial iff ex b₃ being Element of b₁ st b₂ = {b₃} )

proof end;

registration

let c₁ be non trivial 1-sorted ;
cluster non trivial Element of K22(the carrier of a₁);
existence

proof end;

end;

theorem Th3: :: BORSUK_4:3

for b₁ being non trivial set
for b₂ being set ex b₃ being Element of b₁ st b₃ <> b₂

proof end;

registration

let c₁ be non trivial set ;
cluster non trivial Element of K22(a₁);
existence

proof end;

end;

theorem Th4: :: BORSUK_4:4

for b₁ being non trivial set
for b₂ being non trivial Subset of b₁
for b₃ being set ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ <> b₃ )

proof end;

theorem Th5: :: BORSUK_4:5

for b₁, b₂ being Function
for b₃ being set st b₁ is one-to-one & b₂ is one-to-one & (dom b₁) /\ (dom b₂) = {b₃} & (rng b₁) /\ (rng b₂) = {(b₁ . b₃)} holds
b₁ +* b₂ is one-to-one

proof end;

theorem Th6: :: BORSUK_4:6

for b₁, b₂ being Function
for b₃ being set st b₁ is one-to-one & b₂ is one-to-one & (dom b₁) /\ (dom b₂) = {b₃} & (rng b₁) /\ (rng b₂) = {(b₁ . b₃)} & b₁ . b₃ = b₂ . b₃ holds
(b₁ +* b₂) " = (b₁ " ) +* (b₂ " )

proof end;

theorem Th7: :: BORSUK_4:7

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₃,b₄ holds
not b₂ \ {b₃} is empty

proof end;

theorem Th8: :: BORSUK_4:8

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds LSeg b₂,b₃ is convex

proof end;

theorem Th9: :: BORSUK_4:9

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₁ < b₃ & 0 <= b₄ & b₄ <= 1 holds
b₁ <= ((1 - b₄) * b₂) + (b₄ * b₃)

proof end;

theorem Th10: :: BORSUK_4:10

for b₁ being set
for b₂, b₃ being real number holds
( not b₁ in [.b₂,b₃.] or b₁ in ].b₂,b₃.[ or b₁ = b₂ or b₁ = b₃ )

proof end;

theorem Th11: :: BORSUK_4:11

for b₁, b₂, b₃, b₄ being real number st ].b₁,b₂.[ meets [.b₃,b₄.] holds
b₂ > b₃

proof end;

theorem Th12: :: BORSUK_4:12

for b₁, b₂, b₃, b₄ being real number st b₂ <= b₃ holds
[.b₁,b₂.] misses ].b₃,b₄.[

proof end;

theorem Th13: :: BORSUK_4:13

for b₁, b₂, b₃, b₄ being real number st b₂ <= b₃ holds
].b₁,b₂.[ misses [.b₃,b₄.]

proof end;

theorem Th14: :: BORSUK_4:14

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & [.b₁,b₂.] c= [.b₃,b₄.] holds
( b₃ <= b₁ & b₂ <= b₄ )

proof end;

theorem Th15: :: BORSUK_4:15

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & ].b₁,b₂.[ c= [.b₃,b₄.] holds
( b₃ <= b₁ & b₂ <= b₄ )

proof end;

theorem Th16: :: BORSUK_4:16

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & ].b₁,b₂.[ c= [.b₃,b₄.] holds
[.b₁,b₂.] c= [.b₃,b₄.]

proof end;

theorem Th17: :: BORSUK_4:17

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].b₂,b₃.[ holds
[.b₂,b₃.] c= the carrier of I[01]

proof end;

theorem Th18: :: BORSUK_4:18

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].b₂,b₃.] holds
[.b₂,b₃.] c= the carrier of I[01]

proof end;

theorem Th19: :: BORSUK_4:19

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ < b₃ & b₁ = [.b₂,b₃.[ holds
[.b₂,b₃.] c= the carrier of I[01]

proof end;

theorem Th20: :: BORSUK_4:20

for b₁, b₂ being real number st b₁ <> b₂ holds
Cl ].b₁,b₂.] = [.b₁,b₂.]

proof end;

theorem Th21: :: BORSUK_4:21

for b₁, b₂ being real number st b₁ <> b₂ holds
Cl [.b₁,b₂.[ = [.b₁,b₂.]

proof end;

theorem Th22: :: BORSUK_4:22

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].b₂,b₃.[ holds
Cl b₁ = [.b₂,b₃.]

proof end;

theorem Th23: :: BORSUK_4:23

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].b₂,b₃.] holds
Cl b₁ = [.b₂,b₃.]

proof end;

theorem Th24: :: BORSUK_4:24

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ < b₃ & b₁ = [.b₂,b₃.[ holds
Cl b₁ = [.b₂,b₃.]

proof end;

theorem Th25: :: BORSUK_4:25

for b₁, b₂ being real number st b₁ < b₂ holds
[.b₁,b₂.] <> ].b₁,b₂.]

proof end;

theorem Th26: :: BORSUK_4:26

for b₁, b₂ being real number holds
( [.b₁,b₂.[ misses {b₂} & ].b₁,b₂.] misses {b₁} )

proof end;

Lemma21: for b₁, b₂ being real number holds
( ].b₁,b₂.[ misses {b₂} & ].b₁,b₂.[ misses {b₁} )

proof end;

theorem Th27: :: BORSUK_4:27

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] \ {b₁} = ].b₁,b₂.]

proof end;

theorem Th28: :: BORSUK_4:28

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] \ {b₂} = [.b₁,b₂.[

proof end;

theorem Th29: :: BORSUK_4:29

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
].b₁,b₂.] /\ [.b₂,b₃.[ = {b₂}

proof end;

theorem Th30: :: BORSUK_4:30

for b₁, b₂, b₃ being real number holds
( [.b₁,b₂.[ misses [.b₂,b₃.] & [.b₁,b₂.] misses ].b₂,b₃.] )

proof end;

theorem Th31: :: BORSUK_4:31

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
[.b₁,b₃.] \ {b₂} = [.b₁,b₂.[ \/ ].b₂,b₃.]

proof end;

theorem Th32: :: BORSUK_4:32

for b₁ being Subset of I[01]
for b₂, b₃ being real number st b₂ <= b₃ & b₁ = [.b₂,b₃.] holds
( 0 <= b₂ & b₃ <= 1 )

proof end;

theorem Th33: :: BORSUK_4:33

for b₁, b₂ being Subset of I[01]
for b₃, b₄, b₅ being real number st b₃ < b₄ & b₄ < b₅ & b₁ = [.b₃,b₄.[ & b₂ = ].b₄,b₅.] holds
b₁,b₂ are_separated

proof end;

theorem Th34: :: BORSUK_4:34

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] = [.b₁,b₂.[ \/ {b₂}

proof end;

theorem Th35: :: BORSUK_4:35

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] = {b₁} \/ ].b₁,b₂.]

proof end;

theorem Th36: :: BORSUK_4:36

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₂ < b₃ & b₃ <= b₄ holds
[.b₁,b₄.] = ([.b₁,b₂.] \/ ].b₂,b₃.[) \/ [.b₃,b₄.]

proof end;

theorem Th37: :: BORSUK_4:37

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₂ < b₃ & b₃ <= b₄ holds
[.b₁,b₄.] \ ([.b₁,b₂.] \/ [.b₃,b₄.]) = ].b₂,b₃.[

proof end;

theorem Th38: :: BORSUK_4:38

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
].b₁,b₂.] \/ ].b₂,b₃.[ = ].b₁,b₃.[

proof end;

theorem Th39: :: BORSUK_4:39

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
[.b₂,b₃.[ c= ].b₁,b₃.[

proof end;

theorem Th40: :: BORSUK_4:40

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
].b₁,b₂.] \/ [.b₂,b₃.[ = ].b₁,b₃.[

proof end;

theorem Th41: :: BORSUK_4:41

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
].b₁,b₃.[ \ ].b₁,b₂.] = ].b₂,b₃.[

proof end;

theorem Th42: :: BORSUK_4:42

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₂ < b₃ holds
].b₁,b₃.[ \ [.b₂,b₃.[ = ].b₁,b₂.[

proof end;

theorem Th43: :: BORSUK_4:43

for b₁, b₂ being Point of I[01] holds [.b₁,b₂.] is Subset of I[01] by BORSUK_1:83, RCOMP_1:16;

theorem Th44: :: BORSUK_4:44

for b₁, b₂ being Point of I[01] holds ].b₁,b₂.[ is Subset of I[01]

proof end;

theorem Th45: :: BORSUK_4:45

for b₁ being real number holds {b₁} is closed-interval Subset of REAL

proof end;

theorem Th46: :: BORSUK_4:46

for b₁ being non empty connected Subset of I[01]
for b₂, b₃, b₄ being Point of I[01] st b₂ <= b₃ & b₃ <= b₄ & b₂ in b₁ & b₄ in b₁ holds
b₃ in b₁

proof end;

theorem Th47: :: BORSUK_4:47

for b₁ being non empty connected Subset of I[01]
for b₂, b₃ being real number st b₂ in b₁ & b₃ in b₁ holds
[.b₂,b₃.] c= b₁

proof end;

theorem Th48: :: BORSUK_4:48

for b₁, b₂ being real number
for b₃ being Subset of I[01] st b₃ = [.b₁,b₂.] holds
b₃ is closed

proof end;

theorem Th49: :: BORSUK_4:49

for b₁, b₂ being Point of I[01] st b₁ <= b₂ holds
[.b₁,b₂.] is non empty connected compact Subset of I[01]

proof end;

theorem Th50: :: BORSUK_4:50

for b₁ being Subset of I[01]
for b₂ being Subset of REAL st b₂ = b₁ holds
( b₂ is bounded_above & b₂ is bounded_below )

proof end;

theorem Th51: :: BORSUK_4:51

for b₁ being Subset of I[01]
for b₂ being Subset of REAL
for b₃ being real number st b₃ in b₂ & b₂ = b₁ holds
( inf b₂ <= b₃ & b₃ <= sup b₂ )

proof end;

Lemma45: I[01] is closed SubSpace of R^1
by TOPMETR:27, TREAL_1:5;

theorem Th52: :: BORSUK_4:52

for b₁ being Subset of REAL
for b₂ being Subset of I[01] st b₁ = b₂ holds
( b₁ is closed iff b₂ is closed )

proof end;

theorem Th53: :: BORSUK_4:53

for b₁ being closed-interval Subset of REAL holds inf b₁ <= sup b₁

proof end;

theorem Th54: :: BORSUK_4:54

for b₁ being non empty connected compact Subset of I[01]
for b₂ being Subset of REAL st b₁ = b₂ & [.(inf b₂),(sup b₂).] c= b₂ holds
[.(inf b₂),(sup b₂).] = b₂

proof end;

theorem Th55: :: BORSUK_4:55

for b₁ being non empty connected compact Subset of I[01] holds b₁ is closed-interval Subset of REAL

proof end;

theorem Th56: :: BORSUK_4:56

for b₁ being non empty connected compact Subset of I[01] ex b₂, b₃ being Point of I[01] st
( b₂ <= b₃ & b₁ = [.b₂,b₃.] )

proof end;

definition

func I(01) -> non empty strict SubSpace of I[01] means :Def1: :: BORSUK_4:def 1
the carrier of a₁ = ].0,1.[;
existence

proof end;

uniqueness by TSEP_1:5;

end;

:: deftheorem Def1 defines I(01) BORSUK_4:def 1 :

theorem Th57: :: BORSUK_4:57

for b₁ being Subset of I[01] st b₁ = the carrier of I(01) holds
I(01) = I[01] | b₁

proof end;

theorem Th58: :: BORSUK_4:58

the carrier of I(01) = the carrier of I[01] \ {0,1}

proof end;

theorem Th59: :: BORSUK_4:59

I(01) is open SubSpace of I[01] by Th58, JORDAN6:41, TSEP_1:def 1;

theorem Th60: :: BORSUK_4:60

for b₁ being real number holds
( b₁ in the carrier of I(01) iff ( 0 < b₁ & b₁ < 1 ) )

proof end;

theorem Th61: :: BORSUK_4:61

for b₁, b₂ being Point of I[01] st b₁ < b₂ & b₂ <> 1 holds
].b₁,b₂.] is non empty Subset of I(01)

proof end;

theorem Th62: :: BORSUK_4:62

for b₁, b₂ being Point of I[01] st b₁ < b₂ & b₁ <> 0 holds
[.b₁,b₂.[ is non empty Subset of I(01)

proof end;

theorem Th63: :: BORSUK_4:63

for b₁ being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square ,(TOP-REAL 2) | b₁ are_homeomorphic

proof end;

theorem Th64: :: BORSUK_4:64

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₃,b₄ holds
I(01) ,(TOP-REAL b₁) | (b₂ \ {b₃,b₄}) are_homeomorphic

proof end;

theorem Th65: :: BORSUK_4:65

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₃,b₄ holds
I[01] ,(TOP-REAL b₁) | b₂ are_homeomorphic

proof end;

theorem Th66: :: BORSUK_4:66

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ <> b₃ holds
I[01] ,(TOP-REAL b₁) | (LSeg b₂,b₃) are_homeomorphic

proof end;

theorem Th67: :: BORSUK_4:67

for b₁ being Subset of I(01) st ex b₂, b₃ being Point of I[01] st
( b₂ < b₃ & b₁ = [.b₂,b₃.] ) holds
I[01] ,I(01) | b₁ are_homeomorphic

proof end;

theorem Th68: :: BORSUK_4:68

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅, b₆ being Point of I[01] st b₂ is_an_arc_of b₃,b₄ & b₅ < b₆ holds
ex b₇ being non empty Subset of I[01] ex b₈ being Function of (I[01] | b₇),((TOP-REAL b₁) | b₂) st
( b₇ = [.b₅,b₆.] & b₈ is_homeomorphism & b₈ . b₅ = b₃ & b₈ . b₆ = b₄ )

proof end;

theorem Th69: :: BORSUK_4:69

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

proof end;

theorem Th70: :: BORSUK_4:70

for b₁ being Subset of I[01]
for b₂, b₃ being Point of I[01] st b₁ = ].b₂,b₃.[ holds
b₁ is open

proof end;

theorem Th71: :: BORSUK_4:71

for b₁ being Subset of I(01)
for b₂, b₃ being Point of I[01] st b₁ = ].b₂,b₃.[ holds
b₁ is open

proof end;

theorem Th72: :: BORSUK_4:72

for b₁ being Subset of I(01)
for b₂ being Point of I[01] st b₁ = ].0,b₂.] holds
b₁ is closed

proof end;

theorem Th73: :: BORSUK_4:73

for b₁ being Subset of I(01)
for b₂ being Point of I[01] st b₁ = [.b₂,1.[ holds
b₁ is closed

proof end;

theorem Th74: :: BORSUK_4:74

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅, b₆ being Point of I[01] st b₂ is_an_arc_of b₃,b₄ & b₅ < b₆ & b₆ <> 1 holds
ex b₇ being non empty Subset of I(01) ex b₈ being Function of (I(01) | b₇),((TOP-REAL b₁) | (b₂ \ {b₃})) st
( b₇ = ].b₅,b₆.] & b₈ is_homeomorphism & b₈ . b₆ = b₄ )

proof end;

theorem Th75: :: BORSUK_4:75

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅, b₆ being Point of I[01] st b₂ is_an_arc_of b₃,b₄ & b₅ < b₆ & b₅ <> 0 holds
ex b₇ being non empty Subset of I(01) ex b₈ being Function of (I(01) | b₇),((TOP-REAL b₁) | (b₂ \ {b₄})) st
( b₇ = [.b₅,b₆.[ & b₈ is_homeomorphism & b₈ . b₅ = b₃ )

proof end;

theorem Th76: :: BORSUK_4:76

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₄,b₅ & b₃ is_an_arc_of b₅,b₄ & b₂ /\ b₃ = {b₄,b₅} & b₄ <> b₅ holds
I(01) ,(TOP-REAL b₁) | ((b₂ \ {b₄}) \/ (b₃ \ {b₄})) are_homeomorphic

proof end;

theorem Th77: :: BORSUK_4:77

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ holds
(TOP-REAL 2) | (b₁ \ {b₂}), I(01) are_homeomorphic

proof end;

theorem Th78: :: BORSUK_4:78

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ in b₁ & b₃ in b₁ holds
(TOP-REAL 2) | (b₁ \ {b₂}),(TOP-REAL 2) | (b₁ \ {b₃}) are_homeomorphic

proof end;

theorem Th79: :: BORSUK_4:79

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁)
for b₃ being Subset of I(01) st ex b₄, b₅ being Point of I[01] st
( b₄ < b₅ & b₃ = [.b₄,b₅.] ) & I(01) | b₃,(TOP-REAL b₁) | b₂ are_homeomorphic holds
ex b₄, b₅ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₄,b₅

proof end;

theorem Th80: :: BORSUK_4:80

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Function of ((TOP-REAL 2) | b₁),I(01)
for b₃ being non empty Subset of (TOP-REAL 2) st b₂ is_homeomorphism & b₃ c= b₁ & ex b₄, b₅ being Point of I[01] st
( b₄ < b₅ & b₂ .: b₃ = [.b₄,b₅.] ) holds
ex b₄, b₅ being Point of (TOP-REAL 2) st b₃ is_an_arc_of b₄,b₅

proof end;

theorem Th81: :: BORSUK_4:81

for b₁ being Simple_closed_curve
for b₂ being non empty connected compact Subset of (TOP-REAL 2) holds
( not b₂ c= b₁ or b₂ = b₁ or ex b₃, b₄ being Point of (TOP-REAL 2) st b₂ is_an_arc_of b₃,b₄ or ex b₃ being Point of (TOP-REAL 2) st b₂ = {b₃} )

proof end;

registration

cluster the carrier of I[01] -> real-membered ;
coherence by BORSUK_1:83;

end;

Lemma72: for b₁, b₂, b₃, b₄ being real number st ( b₁ <= b₂ or b₃ <= b₄ ) & [.b₁,b₂.] = [.b₃,b₄.] holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th82: :: BORSUK_4:82

for b₁ being non empty compact Subset of I[01] st b₁ c= ].0,1.[ holds
ex b₂ being closed-interval Subset of REAL st
( b₁ c= b₂ & b₂ c= ].0,1.[ & inf b₁ = inf b₂ & sup b₁ = sup b₂ )

proof end;

theorem Th83: :: BORSUK_4:83

for b₁ being non empty compact Subset of I[01] st b₁ c= ].0,1.[ holds
ex b₂, b₃ being Point of I[01] st
( b₂ <= b₃ & b₁ c= [.b₂,b₃.] & [.b₂,b₃.] c= ].0,1.[ )

proof end;

theorem Th84: :: BORSUK_4:84

for b₁ being Simple_closed_curve
for b₂ being closed Subset of (TOP-REAL 2) st b₂ c= b₁ & b₂ <> b₁ holds
ex b₃, b₄ being Point of (TOP-REAL 2)ex b₅ being Subset of (TOP-REAL 2) st
( b₅ is_an_arc_of b₃,b₄ & b₂ c= b₅ & b₅ c= b₁ )

proof end;