:: by Adam Grabowski

::

:: Received June 12, 2003

:: Copyright (c) 2003-2019 Association of Mizar Users

::$CT

theorem Th2: :: BORSUK_5:3

for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3,x4,x5,x6 are_mutually_distinct holds

card {x1,x2,x3,x4,x5,x6} = 6

card {x1,x2,x3,x4,x5,x6} = 6

proof end;

theorem :: BORSUK_5:4

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct holds

card {x1,x2,x3,x4,x5,x6,x7} = 7

card {x1,x2,x3,x4,x5,x6,x7} = 7

proof end;

theorem Th4: :: BORSUK_5:5

for x1, x2, x3, x4, x5, x6 being set st {x1,x2,x3} misses {x4,x5,x6} holds

( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )

( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )

proof end;

theorem :: BORSUK_5:6

for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3 are_mutually_distinct & x4,x5,x6 are_mutually_distinct & {x1,x2,x3} misses {x4,x5,x6} holds

x1,x2,x3,x4,x5,x6 are_mutually_distinct

x1,x2,x3,x4,x5,x6 are_mutually_distinct

proof end;

theorem :: BORSUK_5:7

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6 are_mutually_distinct & {x1,x2,x3,x4,x5,x6} misses {x7} holds

x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct

x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct

proof end;

theorem :: BORSUK_5:8

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct holds

x7,x1,x2,x3,x4,x5,x6 are_mutually_distinct

x7,x1,x2,x3,x4,x5,x6 are_mutually_distinct

proof end;

theorem :: BORSUK_5:9

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct holds

x1,x2,x5,x3,x6,x7,x4 are_mutually_distinct

x1,x2,x5,x3,x6,x7,x4 are_mutually_distinct

proof end;

Lm1: R^1 is pathwise_connected

proof end;

registration
end;

theorem :: BORSUK_5:10

for A, B being Subset of R^1

for a, b, c, d being Real st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds

A,B are_separated

for a, b, c, d being Real st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds

A,B are_separated

proof end;

registration
end;

theorem :: BORSUK_5:13

definition

let a, b be Real;

coherence

RAT /\ ].a,b.[ is Subset of REAL ;

coherence

IRRAT /\ ].a,b.[ is Subset of REAL ;

end;
coherence

RAT /\ ].a,b.[ is Subset of REAL ;

coherence

IRRAT /\ ].a,b.[ is Subset of REAL ;

:: deftheorem defines IRRAT BORSUK_5:def 3 :

for a, b being Real holds IRRAT (a,b) = IRRAT /\ ].a,b.[;

for a, b being Real holds IRRAT (a,b) = IRRAT /\ ].a,b.[;

registration

let a be Rational;

let b be irrational Real;

coherence

a + b is irrational

b + a is irrational ;

end;
let b be irrational Real;

coherence

a + b is irrational

proof end;

coherence b + a is irrational ;

registration
end;

registration

let a be Rational;

let b be irrational Real;

coherence

a - b is irrational

b - a is irrational

end;
let b be irrational Real;

coherence

a - b is irrational

proof end;

coherence b - a is irrational

proof end;

registration
end;

registration

let a be non zero Rational;

let b be irrational Real;

coherence

a * b is irrational by Th21;

coherence

b * a is irrational ;

coherence

a / b is irrational by Th23;

coherence

b / a is irrational by Th22;

end;
let b be irrational Real;

coherence

a * b is irrational by Th21;

coherence

b * a is irrational ;

coherence

a / b is irrational by Th23;

coherence

b / a is irrational by Th22;

Lm2: for A being Subset of R^1

for a, b being Real st a < b & A = RAT (a,b) holds

( a in Cl A & b in Cl A )

proof end;

Lm3: for A being Subset of R^1

for a, b being Real st a < b & A = IRRAT (a,b) holds

( a in Cl A & b in Cl A )

proof end;

theorem :: BORSUK_5:37

for A being Subset of R^1

for a, b, c being Real st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds

Cl A = [.a,c.]

for a, b, c being Real st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds

Cl A = [.a,c.]

proof end;

Lm4: for a being Real holds ].-infty,a.] is closed

proof end;

Lm5: for a being Real holds [.a,+infty.[ is closed

proof end;

registration

let A, B be open Subset of REAL;

reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;

coherence

for b_{1} being Subset of REAL st b_{1} = A /\ B holds

b_{1} is open

for b_{1} being Subset of REAL st b_{1} = A \/ B holds

b_{1} is open

end;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;

coherence

for b

b

proof end;

coherence for b

b

proof end;

Lm6: for a, b being ExtReal holds ].a,b.[ is open

proof end;

registration

let a be Real;

coherence

not ].a,+infty.[ is empty

not ].-infty,a.] is empty by XXREAL_1:234;

coherence

not ].-infty,a.[ is empty

not [.a,+infty.[ is empty by XXREAL_1:236;

end;
coherence

not ].a,+infty.[ is empty

proof end;

coherence not ].-infty,a.] is empty by XXREAL_1:234;

coherence

not ].-infty,a.[ is empty

proof end;

coherence not [.a,+infty.[ is empty by XXREAL_1:236;

theorem Th52: :: BORSUK_5:53

for A, B being Subset of R^1

for b being Real st A = ].-infty,b.[ & B = ].b,+infty.[ holds

A,B are_separated

for b being Real st A = ].-infty,b.[ & B = ].b,+infty.[ holds

A,B are_separated

proof end;

theorem :: BORSUK_5:54

for A being Subset of R^1

for a, b being Real st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds

Cl A = [.a,+infty.[

for a, b being Real st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds

Cl A = [.a,+infty.[

proof end;

theorem Th54: :: BORSUK_5:55

for A being Subset of R^1

for a, b being Real st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds

Cl A = [.a,+infty.[

for a, b being Real st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds

Cl A = [.a,+infty.[

proof end;

theorem :: BORSUK_5:56

for A being Subset of R^1

for a, b, c being Real st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds

Cl A = [.a,+infty.[

for a, b, c being Real st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds

Cl A = [.a,+infty.[

proof end;

theorem :: BORSUK_5:60

for A being Subset of R^1 st A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ holds

A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}

A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}

proof end;

theorem :: BORSUK_5:61

Lm7: ((IRRAT (2,4)) \/ {4}) \/ {5} c= ].1,+infty.[

proof end;

Lm8: ].1,+infty.[ c= [.1,+infty.[

by XXREAL_1:45;

Lm9: ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[

proof end;

Lm10: ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}

proof end;

theorem :: BORSUK_5:62

(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5}

proof end;

theorem :: BORSUK_5:63

for A being Subset of R^1

for a, b being Real st a <= b & A = {a} \/ [.b,+infty.[ holds

A ` = ].-infty,a.[ \/ ].a,b.[

for a, b being Real st a <= b & A = {a} \/ [.b,+infty.[ holds

A ` = ].-infty,a.[ \/ ].a,b.[

proof end;

theorem :: BORSUK_5:64

for A being Subset of R^1

for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds

Cl A = ].-infty,b.]

for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds

Cl A = ].-infty,b.]

proof end;

theorem Th64: :: BORSUK_5:65

for A being Subset of R^1

for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.] holds

Cl A = ].-infty,b.]

for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.] holds

Cl A = ].-infty,b.]

proof end;

theorem Th65: :: BORSUK_5:66

for A being Subset of R^1

for a, b, c being Real st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds

Cl A = ].-infty,c.]

for a, b, c being Real st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds

Cl A = ].-infty,c.]

proof end;

theorem :: BORSUK_5:67

for A being Subset of R^1

for a, b, c, d being Real st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds

Cl A = ].-infty,c.] \/ {d}

for a, b, c, d being Real st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds

Cl A = ].-infty,c.] \/ {d}

proof end;

theorem :: BORSUK_5:68

for A being Subset of R^1

for a, b being Real st a <= b & A = ].-infty,a.] \/ {b} holds

A ` = ].a,b.[ \/ ].b,+infty.[

for a, b being Real st a <= b & A = ].-infty,a.] \/ {b} holds

A ` = ].a,b.[ \/ ].b,+infty.[

proof end;

theorem Th72: :: BORSUK_5:73

for X being compact Subset of R^1

for X9 being Subset of REAL st X9 = X holds

( X9 is bounded_above & X9 is bounded_below )

for X9 being Subset of REAL st X9 = X holds

( X9 is bounded_above & X9 is bounded_below )

proof end;

theorem Th73: :: BORSUK_5:74

for X being compact Subset of R^1

for X9 being Subset of REAL

for x being Real st x in X9 & X9 = X holds

( lower_bound X9 <= x & x <= upper_bound X9 )

for X9 being Subset of REAL

for x being Real st x in X9 & X9 = X holds

( lower_bound X9 <= x & x <= upper_bound X9 )

proof end;

theorem Th74: :: BORSUK_5:75

for C being non empty connected compact Subset of R^1

for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds

[.(lower_bound C9),(upper_bound C9).] = C9

for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds

[.(lower_bound C9),(upper_bound C9).] = C9

proof end;

theorem Th75: :: BORSUK_5:76

for A being connected Subset of R^1

for a, b, c being Real st a <= b & b <= c & a in A & c in A holds

b in A

for a, b, c being Real st a <= b & b <= c & a in A & c in A holds

b in A

proof end;

theorem Th77: :: BORSUK_5:78

for X being non empty connected compact Subset of R^1 holds X is non empty closed_interval Subset of REAL

proof end;

theorem :: BORSUK_5:79

for A being non empty connected compact Subset of R^1 ex a, b being Real st

( a <= b & A = [.a,b.] )

( a <= b & A = [.a,b.] )

proof end;

registration

let T be TopSpace;

existence

ex b_{1} being Subset-Family of T st

( b_{1} is open & b_{1} is closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;