:: by Andrzej Trybulec, Yatsuka Nakamura, Artur Korni{\l}owicz and

::

:: Received January 22, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

begin

definition

let r, s be ext-real number ;

coherence

{ a where a is Element of ExtREAL : ( r <= a & a <= s ) } is set ;

;

coherence

{ a where a is Element of ExtREAL : ( r <= a & a < s ) } is set ;

;

coherence

{ a where a is Element of ExtREAL : ( r < a & a <= s ) } is set ;

;

coherence

{ a where a is Element of ExtREAL : ( r < a & a < s ) } is set ;

;

end;
func [.r,s.] -> set equals :: XXREAL_1:def 1

{ a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;

correctness { a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;

coherence

{ a where a is Element of ExtREAL : ( r <= a & a <= s ) } is set ;

;

func [.r,s.[ -> set equals :: XXREAL_1:def 2

{ a where a is Element of ExtREAL : ( r <= a & a < s ) } ;

correctness { a where a is Element of ExtREAL : ( r <= a & a < s ) } ;

coherence

{ a where a is Element of ExtREAL : ( r <= a & a < s ) } is set ;

;

func ].r,s.] -> set equals :: XXREAL_1:def 3

{ a where a is Element of ExtREAL : ( r < a & a <= s ) } ;

correctness { a where a is Element of ExtREAL : ( r < a & a <= s ) } ;

coherence

{ a where a is Element of ExtREAL : ( r < a & a <= s ) } is set ;

;

func ].r,s.[ -> set equals :: XXREAL_1:def 4

{ a where a is Element of ExtREAL : ( r < a & a < s ) } ;

correctness { a where a is Element of ExtREAL : ( r < a & a < s ) } ;

coherence

{ a where a is Element of ExtREAL : ( r < a & a < s ) } is set ;

;

:: deftheorem defines [. XXREAL_1:def 1 :

for r, s being ext-real number holds [.r,s.] = { a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;

for r, s being ext-real number holds [.r,s.] = { a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;

:: deftheorem defines [. XXREAL_1:def 2 :

for r, s being ext-real number holds [.r,s.[ = { a where a is Element of ExtREAL : ( r <= a & a < s ) } ;

for r, s being ext-real number holds [.r,s.[ = { a where a is Element of ExtREAL : ( r <= a & a < s ) } ;

:: deftheorem defines ]. XXREAL_1:def 3 :

for r, s being ext-real number holds ].r,s.] = { a where a is Element of ExtREAL : ( r < a & a <= s ) } ;

for r, s being ext-real number holds ].r,s.] = { a where a is Element of ExtREAL : ( r < a & a <= s ) } ;

:: deftheorem defines ]. XXREAL_1:def 4 :

for r, s being ext-real number holds ].r,s.[ = { a where a is Element of ExtREAL : ( r < a & a < s ) } ;

for r, s being ext-real number holds ].r,s.[ = { a where a is Element of ExtREAL : ( r < a & a < s ) } ;

registration

let r, s be ext-real number ;

coherence

[.r,s.] is ext-real-membered

[.r,s.[ is ext-real-membered

].r,s.] is ext-real-membered

].r,s.[ is ext-real-membered

end;
coherence

[.r,s.] is ext-real-membered

proof end;

coherence [.r,s.[ is ext-real-membered

proof end;

coherence ].r,s.] is ext-real-membered

proof end;

coherence ].r,s.[ is ext-real-membered

proof end;

theorem Th5: :: XXREAL_1:5

for x being set

for p, q being ext-real number holds

( not x in [.p,q.] or x in ].p,q.[ or x = p or x = q )

for p, q being ext-real number holds

( not x in [.p,q.] or x in ].p,q.[ or x = p or x = q )

proof end;

theorem :: XXREAL_1:10

for x being set

for p, q being ext-real number holds

( not x in [.p,q.[ or ( x in ].p,q.] & x <> q ) or x = p )

for p, q being ext-real number holds

( not x in [.p,q.[ or ( x in ].p,q.] & x <> q ) or x = p )

proof end;

theorem :: XXREAL_1:11

for x being set

for p, q being ext-real number holds

( not x in ].p,q.] or ( x in [.p,q.[ & x <> p ) or x = q )

for p, q being ext-real number holds

( not x in ].p,q.] or ( x in [.p,q.[ & x <> p ) or x = q )

proof end;

theorem Th16: :: XXREAL_1:16

for x being set

for p, q being ext-real number st x in ].p,q.[ holds

( x in [.p,q.] & x <> p & x <> q )

for p, q being ext-real number st x in ].p,q.[ holds

( x in [.p,q.] & x <> p & x <> q )

proof end;

registration

let r be ext-real number ;

coherence

not [.r,r.] is empty

[.r,r.[ is empty by Th18;

coherence

].r,r.] is empty by Th19;

coherence

].r,r.[ is empty by Th20;

end;
coherence

not [.r,r.] is empty

proof end;

coherence [.r,r.[ is empty by Th18;

coherence

].r,r.] is empty by Th19;

coherence

].r,r.[ is empty by Th20;

begin

theorem :: XXREAL_1:162

for r, s, p, q being ext-real number st [.r,s.[ meets [.p,q.[ holds

[.r,s.[ \/ [.p,q.[ = [.(min (r,p)),(max (s,q)).[

[.r,s.[ \/ [.p,q.[ = [.(min (r,p)),(max (s,q)).[

proof end;

theorem :: XXREAL_1:164

for r, s, p, q being ext-real number st ].r,s.] meets ].p,q.] holds

].r,s.] \/ ].p,q.] = ].(min (r,p)),(max (s,q)).]

].r,s.] \/ ].p,q.] = ].(min (r,p)),(max (s,q)).]

proof end;

theorem :: XXREAL_1:179

for p, r, s, q being ext-real number st p <= r & p <= s & r <= q & s <= q holds

([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.]

([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.]

proof end;

theorem :: XXREAL_1:180

for p, r, s, q being ext-real number st p < r & p < s & r < q & s < q holds

(].p,r.] \/ ].r,s.[) \/ [.s,q.[ = ].p,q.[

(].p,r.] \/ ].r,s.[) \/ [.s,q.[ = ].p,q.[

proof end;

theorem :: XXREAL_1:181

for p, r, s, q being ext-real number st p <= r & r <= s & s <= q holds

([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.]

([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.]

proof end;

theorem :: XXREAL_1:198

for p, q, r, s being ext-real number st [.p,q.[ meets [.r,s.[ holds

[.p,q.[ \ [.r,s.[ = [.p,r.[ \/ [.s,q.[

[.p,q.[ \ [.r,s.[ = [.p,r.[ \/ [.s,q.[

proof end;

theorem :: XXREAL_1:199

for p, q, r, s being ext-real number st ].p,q.] meets ].r,s.] holds

].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.]

].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.]

proof end;

theorem :: XXREAL_1:200

for p, r, s, q being ext-real number st p <= r & s <= q holds

[.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[

[.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[

proof end;

begin

begin

:: from LIMFUNC1, 2008.06.12, A.T.

registration
end;

registration
end;

registration
end;

:: from LIMFUNC1,2008.06.13, A.T.

theorem :: XXREAL_1:242

theorem :: XXREAL_1:243

theorem :: XXREAL_1:248

theorem :: XXREAL_1:260

theorem :: XXREAL_1:261

theorem :: XXREAL_1:264

theorem :: XXREAL_1:281

theorem :: XXREAL_1:282

theorem :: XXREAL_1:283

theorem :: XXREAL_1:284

theorem :: XXREAL_1:285

theorem Th300: :: XXREAL_1:300

for r, s, p, q being ext-real number st r <= s & p <= q holds

[.r,q.] \ ].p,s.[ = [.r,p.] \/ [.s,q.]

[.r,q.] \ ].p,s.[ = [.r,p.] \/ [.s,q.]

proof end;

theorem Th302: :: XXREAL_1:302

for r, s, p, q being ext-real number st r <= s & p <= q holds

[.r,q.[ \ [.p,s.[ = [.r,p.[ \/ [.s,q.[

[.r,q.[ \ [.p,s.[ = [.r,p.[ \/ [.s,q.[

proof end;

theorem Th304: :: XXREAL_1:304

for r, s, p, q being ext-real number st r <= s & p <= q holds

[.r,q.] \ [.p,s.[ = [.r,p.[ \/ [.s,q.]

[.r,q.] \ [.p,s.[ = [.r,p.[ \/ [.s,q.]

proof end;

theorem Th308: :: XXREAL_1:308

for r, s, p, q being ext-real number st r <= s & p <= q holds

[.r,q.] \ ].p,s.] = [.r,p.] \/ ].s,q.]

[.r,q.] \ ].p,s.] = [.r,p.] \/ ].s,q.]

proof end;

theorem Th309: :: XXREAL_1:309

for r, s, p, q being ext-real number st r <= s & p <= q holds

].r,q.[ \ [.p,s.] = ].r,p.[ \/ ].s,q.[

].r,q.[ \ [.p,s.] = ].r,p.[ \/ ].s,q.[

proof end;

theorem Th310: :: XXREAL_1:310

for r, s, p, q being ext-real number st r <= s & p <= q holds

[.r,q.[ \ [.p,s.] = [.r,p.[ \/ ].s,q.[

[.r,q.[ \ [.p,s.] = [.r,p.[ \/ ].s,q.[

proof end;

theorem Th312: :: XXREAL_1:312

for r, s, p, q being ext-real number st r <= s & p <= q holds

[.r,q.] \ [.p,s.] = [.r,p.[ \/ ].s,q.]

[.r,q.] \ [.p,s.] = [.r,p.[ \/ ].s,q.]

proof end;

theorem Th333: :: XXREAL_1:333

for p, q being ext-real number

for s being real number st p < q holds

].-infty,q.[ \ ].p,s.[ = ].-infty,p.] \/ [.s,q.[

for s being real number st p < q holds

].-infty,q.[ \ ].p,s.[ = ].-infty,p.] \/ [.s,q.[

proof end;

theorem Th334: :: XXREAL_1:334

for p, q being ext-real number

for s being real number st p <= q holds

].-infty,q.] \ ].p,s.[ = ].-infty,p.] \/ [.s,q.]

for s being real number st p <= q holds

].-infty,q.] \ ].p,s.[ = ].-infty,p.] \/ [.s,q.]

proof end;

theorem Th335: :: XXREAL_1:335

for p, q being ext-real number

for s being real number st p <= q holds

].-infty,q.[ \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.[

for s being real number st p <= q holds

].-infty,q.[ \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.[

proof end;

theorem Th336: :: XXREAL_1:336

for p, q being ext-real number

for s being real number st p <= q holds

].-infty,q.] \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.]

for s being real number st p <= q holds

].-infty,q.] \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.]

proof end;

theorem Th337: :: XXREAL_1:337

for p, q being ext-real number

for s being real number st p < q holds

].-infty,q.[ \ ].p,s.] = ].-infty,p.] \/ ].s,q.[

for s being real number st p < q holds

].-infty,q.[ \ ].p,s.] = ].-infty,p.] \/ ].s,q.[

proof end;

theorem Th338: :: XXREAL_1:338

for p, q being ext-real number

for s being real number st p <= q holds

].-infty,q.] \ ].p,s.] = ].-infty,p.] \/ ].s,q.]

for s being real number st p <= q holds

].-infty,q.] \ ].p,s.] = ].-infty,p.] \/ ].s,q.]

proof end;

theorem Th340: :: XXREAL_1:340

for p, q being ext-real number

for s being real number st p <= q holds

].-infty,q.] \ [.p,s.] = ].-infty,p.[ \/ ].s,q.]

for s being real number st p <= q holds

].-infty,q.] \ [.p,s.] = ].-infty,p.[ \/ ].s,q.]

proof end;

theorem :: XXREAL_1:347

for s being ext-real number

for q being real number holds [.-infty,q.[ \ ].-infty,s.[ = {-infty} \/ [.s,q.[

for q being real number holds [.-infty,q.[ \ ].-infty,s.[ = {-infty} \/ [.s,q.[

proof end;

theorem :: XXREAL_1:348

for s being ext-real number

for q being real number holds [.-infty,q.[ \ ].-infty,s.] = {-infty} \/ ].s,q.[

for q being real number holds [.-infty,q.[ \ ].-infty,s.] = {-infty} \/ ].s,q.[

proof end;

theorem Th350: :: XXREAL_1:350

for q being ext-real number

for p being real number st p <= q holds

].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.]

for p being real number st p <= q holds

].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.]

proof end;

theorem :: XXREAL_1:351

for p being ext-real number

for q being real number st p <= q holds

].-infty,q.] \ ].p,q.[ = ].-infty,p.] \/ {q}

for q being real number st p <= q holds

].-infty,q.] \ ].p,q.[ = ].-infty,p.] \/ {q}

proof end;

theorem :: XXREAL_1:352

for p being ext-real number

for q being real number st p <= q holds

].-infty,q.] \ [.p,q.[ = ].-infty,p.[ \/ {q}

for q being real number st p <= q holds

].-infty,q.] \ [.p,q.[ = ].-infty,p.[ \/ {q}

proof end;

theorem :: XXREAL_1:353

theorem :: XXREAL_1:355

theorem :: XXREAL_1:357

theorem :: XXREAL_1:359

theorem :: XXREAL_1:363

theorem :: XXREAL_1:367

theorem :: XXREAL_1:371

for p being ext-real number

for r being real number holds ].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}

for r being real number holds ].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}

proof end;

theorem :: XXREAL_1:372

for p being ext-real number

for r being real number holds ].r,+infty.] \ [.p,+infty.[ = ].r,p.[ \/ {+infty}

for r being real number holds ].r,+infty.] \ [.p,+infty.[ = ].r,p.[ \/ {+infty}

proof end;

theorem :: XXREAL_1:375

theorem :: XXREAL_1:376

theorem :: XXREAL_1:377

theorem :: XXREAL_1:378

theorem :: XXREAL_1:379

theorem :: XXREAL_1:380

theorem :: XXREAL_1:381

theorem :: XXREAL_1:382

theorem :: XXREAL_1:383

theorem :: XXREAL_1:384

theorem :: XXREAL_1:385

theorem :: XXREAL_1:386

theorem :: XXREAL_1:387

theorem :: XXREAL_1:388

theorem :: XXREAL_1:389

theorem :: XXREAL_1:390

theorem :: XXREAL_1:391

for r, s being ext-real number

for p being real number st r < s holds

].r,+infty.[ \ ].p,s.[ = ].r,p.] \/ [.s,+infty.[

for p being real number st r < s holds

].r,+infty.[ \ ].p,s.[ = ].r,p.] \/ [.s,+infty.[

proof end;

theorem :: XXREAL_1:392

for r, s being ext-real number

for p being real number st r <= s holds

[.r,+infty.[ \ ].p,s.[ = [.r,p.] \/ [.s,+infty.[

for p being real number st r <= s holds

[.r,+infty.[ \ ].p,s.[ = [.r,p.] \/ [.s,+infty.[

proof end;

theorem :: XXREAL_1:393

for r, s being ext-real number

for p being real number st r < s holds

].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[

for p being real number st r < s holds

].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[

proof end;

theorem :: XXREAL_1:394

for r, s being ext-real number

for p being real number st r <= s holds

[.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[

for p being real number st r <= s holds

[.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[

proof end;

theorem :: XXREAL_1:395

for s being ext-real number

for p being real number st p <= s holds

[.p,+infty.[ \ ].p,s.] = {p} \/ ].s,+infty.[

for p being real number st p <= s holds

[.p,+infty.[ \ ].p,s.] = {p} \/ ].s,+infty.[

proof end;

theorem :: XXREAL_1:396

for s being ext-real number

for p being real number holds [.-infty,+infty.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.[

for p being real number holds [.-infty,+infty.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.[

proof end;

theorem :: XXREAL_1:397

for s being ext-real number

for p being real number holds [.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[

for p being real number holds [.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[

proof end;

theorem :: XXREAL_1:400

for s being ext-real number

for p being real number st p <= s holds

[.p,+infty.[ \ ].p,s.[ = {p} \/ [.s,+infty.[

for p being real number st p <= s holds

[.p,+infty.[ \ ].p,s.[ = {p} \/ [.s,+infty.[

proof end;

:: analogous to Th165

:: analogous to Th138

:: special cases of Th128-Th132

theorem :: XXREAL_1:419

theorem :: XXREAL_1:420

theorem :: XXREAL_1:421

theorem :: XXREAL_1:424

theorem :: XXREAL_1:425

theorem :: XXREAL_1:426