Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Half Open Intervals in Real Numbers

by
Yatsuka Nakamura

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.];

```