The abstract of the Mizar article:

Half Open Intervals in Real Numbers

by

Yatsuka Nakamura

Received February 1, 2002

MML identifier: RCOMP_2

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, BOOLE, SQUARE_1, RCOMP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
      SQUARE_1, RCOMP_1;
 constructors SQUARE_1, RCOMP_1, XCMPLX_0, MEMBERED;
 clusters XREAL_0, MEMBERED;
 requirements SUBSET, BOOLE;


begin

 reserve s,g,h,r,p,p1,p2,q,q1,q2,x,y,z for real number;

canceled;

theorem :: RCOMP_2:2
 y < x & z < x iff max(y,z) < x;

definition let g,s be real number;
  func [. g,s .[ -> Subset of REAL equals
:: RCOMP_2:def 1
   { r where r is Real : g<=r & r<s };
  func ]. g,s .] -> Subset of REAL equals
:: RCOMP_2:def 2
   { r where r is Real : g<r & r<=s };
end;

theorem :: RCOMP_2:3
r in [.p,q.[ iff p<=r & r<q;

theorem :: RCOMP_2:4
r in ].p,q.] iff p<r & r<=q;

:: Note: r in [.p,q.] iff p<=r & r<=q by TOPREAL5:1
::       r in ].p,q.[ iff p<r & r<q by JORDAN6:45

theorem :: RCOMP_2:5
  for g,s st g<s holds [.g,s.[ = ].g,s.[ \/ {g};

theorem :: RCOMP_2:6
  for g,s st g<s holds ].g,s.] = ].g,s.[ \/ {s};

theorem :: RCOMP_2:7
   [.g,g.[ = {};

theorem :: RCOMP_2:8
   ].g,g.] = {};

theorem :: RCOMP_2:9
  p <= g implies [.g,p.[ = {};

theorem :: RCOMP_2:10
  p <= g implies ].g,p.] = {};

theorem :: RCOMP_2:11
  g <= p & p<=h implies [.g,p.[ \/ [.p,h.[ = [.g,h.[;

theorem :: RCOMP_2:12
  g <= p & p<=h implies ].g,p.] \/ ].p,h.] = ].g,h.];

theorem :: RCOMP_2:13
g<=p1 & g<=p2 & p1<=h & p2<=h implies
   [.g,h.] = [.g,p1.[ \/ [.p1,p2.] \/ ].p2,h.];

theorem :: RCOMP_2:14
g<p1 & g<p2 & p1<h & p2<h implies
   ].g,h.[ = ].g,p1.] \/ ].p1,p2.[ \/ [.p2,h.[;

theorem :: RCOMP_2:15
[.q1,q2.[ /\ [.p1,p2.[ = [.max(q1,p1),min(q2,p2).[;

theorem :: RCOMP_2:16
].q1,q2.] /\ ].p1,p2.] = ].max(q1,p1),min(q2,p2).];

theorem :: RCOMP_2:17
].p,q.[ c= [.p,q.[ & ].p,q.[ c= ].p,q.]
  & [.p,q.[ c= [.p,q.] & ].p,q.] c= [.p,q.];

theorem :: RCOMP_2:18
  r in [.p,g.[ & s in [.p,g.[ implies [.r,s.] c= [.p,g.[;

theorem :: RCOMP_2:19
  r in ].p,g.] & s in ].p,g.] implies [.r,s.] c= ].p,g.];

theorem :: RCOMP_2:20
p<=q & q<=r implies [.p,q.] \/ ].q,r.] = [.p,r.];

theorem :: RCOMP_2:21
p<=q & q<=r implies [.p,q.[ \/ [.q,r.] = [.p,r.];

theorem :: RCOMP_2:22
[.q1,q2.[ meets [.p1,p2.[ implies q2>=p1;

theorem :: RCOMP_2:23
].q1,q2.] meets ].p1,p2.] implies q2>=p1;

theorem :: RCOMP_2:24
[.q1,q2.[ meets [.p1,p2.[ implies
    [.q1,q2.[ \/ [.p1,p2.[ = [.min(q1,p1),max(q2,p2).[;

theorem :: RCOMP_2:25
].q1,q2.] meets ].p1,p2.] implies
    ].q1,q2.] \/ ].p1,p2.] = ].min(q1,p1),max(q2,p2).];

theorem :: RCOMP_2:26
[.p1,p2.[ meets [.q1,q2.[ implies
  [.p1,p2.[ \ [.q1,q2.[ = [.p1,q1.[ \/ [.q2,p2.[;

theorem :: RCOMP_2:27
].p1,p2.] meets ].q1,q2.] implies
  ].p1,p2.] \ ].q1,q2.] = ].p1,q1.] \/ ].q2,p2.];