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

::

:: Received January 22, 2007

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

definition

let r, s be ExtReal;

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 ExtReal holds [.r,s.] = { a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;

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

:: deftheorem defines [. XXREAL_1:def 2 :

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

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

:: deftheorem defines ]. XXREAL_1:def 3 :

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

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

:: deftheorem defines ]. XXREAL_1:def 4 :

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

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

registration

let r, s be ExtReal;

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 :: XXREAL_1:10

for x being set

for p, q being ExtReal holds

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

for p, q being ExtReal 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 ExtReal holds

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

for p, q being ExtReal holds

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

proof end;

registration

let r be ExtReal;

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;

theorem :: XXREAL_1:162

for p, q, r, s being ExtReal 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 p, q, r, s being ExtReal 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, q, r, s being ExtReal 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, q, r, s being ExtReal 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, q, r, s being ExtReal 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;

:: from LIMFUNC1, 2008.06.12, A.T.

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 Th333: :: XXREAL_1:333

for p, q being ExtReal

for s being Real st p < q holds

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

for s being Real st p < q holds

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

proof end;

theorem Th334: :: XXREAL_1:334

for p, q being ExtReal

for s being Real st p <= q holds

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

for s being Real st p <= q holds

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

proof end;

theorem Th335: :: XXREAL_1:335

for p, q being ExtReal

for s being Real st p <= q holds

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

for s being Real st p <= q holds

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

proof end;

theorem Th336: :: XXREAL_1:336

for p, q being ExtReal

for s being Real st p <= q holds

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

for s being Real st p <= q holds

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

proof end;

theorem Th337: :: XXREAL_1:337

for p, q being ExtReal

for s being Real st p < q holds

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

for s being Real st p < q holds

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

proof end;

theorem Th338: :: XXREAL_1:338

for p, q being ExtReal

for s being Real st p <= q holds

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

for s being Real st p <= q holds

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

proof end;

theorem Th340: :: XXREAL_1:340

for p, q being ExtReal

for s being Real st p <= q holds

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

for s being Real st p <= q holds

].-infty,q.] \ [.p,s.] = ].-infty,p.[ \/ ].s,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: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 ExtReal

for p being Real st r < s holds

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

for p being Real st r < s holds

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

proof end;

theorem :: XXREAL_1:392

for r, s being ExtReal

for p being Real st r <= s holds

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

for p being Real st r <= s holds

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

proof end;

theorem :: XXREAL_1:393

for r, s being ExtReal

for p being Real st r < s holds

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

for p being Real st r < s holds

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

proof end;

theorem :: XXREAL_1:394

for r, s being ExtReal

for p being Real st r <= s holds

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

for p being Real st r <= s holds

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

proof end;

theorem :: XXREAL_1:396

for s being ExtReal

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

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

proof end;

theorem :: XXREAL_1:397

for s being ExtReal

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

for p being Real holds [.-infty,+infty.[ \ ].p,s.] = [.-infty,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