let A be Interval; for x being Real holds
( A is open_interval iff x ++ A is open_interval )
let x be Real; ( A is open_interval iff x ++ A is open_interval )
reconsider y = - x as Element of REAL by XREAL_0:def 1;
A1:
for B being Interval
for y being Real st B is open_interval holds
y ++ B is open_interval
proof
let B be
Interval;
for y being Real st B is open_interval holds
y ++ B is open_interval let y be
Real;
( B is open_interval implies y ++ B is open_interval )
reconsider y =
y as
Element of
REAL by XREAL_0:def 1;
reconsider z =
y as
R_eal by XXREAL_0:def 1;
assume
B is
open_interval
;
y ++ B is open_interval
then consider a,
b being
R_eal such that A2:
B = ].a,b.[
by MEASURE5:def 2;
reconsider s =
z + a,
t =
z + b as
R_eal ;
y ++ B = ].s,t.[
proof
thus
y ++ B c= ].s,t.[
XBOOLE_0:def 10 ].s,t.[ c= y ++ Bproof
let c be
object ;
TARSKI:def 3 ( not c in y ++ B or c in ].s,t.[ )
assume A3:
c in y ++ B
;
c in ].s,t.[
then reconsider c =
c as
Element of
REAL ;
consider d being
Real such that A4:
d in B
and A5:
c = y + d
by A3, Lm1;
reconsider d1 =
d as
R_eal by XXREAL_0:def 1;
a < d1
by A2, A4, MEASURE5:def 1;
then A6:
s < z + d1
by XXREAL_3:43;
d1 < b
by A2, A4, MEASURE5:def 1;
then A7:
z + d1 < t
by XXREAL_3:43;
z + d1 = c
by A5, SUPINF_2:1;
hence
c in ].s,t.[
by A6, A7;
verum
end;
let c be
object ;
TARSKI:def 3 ( not c in ].s,t.[ or c in y ++ B )
assume A8:
c in ].s,t.[
;
c in y ++ B
then reconsider c =
c as
Element of
REAL ;
reconsider c1 =
c as
R_eal by XXREAL_0:def 1;
A9:
c = y + (c - y)
;
c1 < z + b
by A8, MEASURE5:def 1;
then
c1 - z < (b + z) - z
by XXREAL_3:43;
then A10:
c1 - z < b
by XXREAL_3:22;
z + a < c1
by A8, MEASURE5:def 1;
then
(a + z) - z < c1 - z
by XXREAL_3:43;
then A11:
a < c1 - z
by XXREAL_3:22;
c1 - z = c - y
by SUPINF_2:3;
then
c - y in B
by A2, A11, A10;
hence
c in y ++ B
by A9, Lm1;
verum
end;
hence
y ++ B is
open_interval
by MEASURE5:def 2;
verum
end;
hence
( A is open_interval implies x ++ A is open_interval )
; ( x ++ A is open_interval implies A is open_interval )
assume A12:
x ++ A is open_interval
; A is open_interval
then reconsider B = x ++ A as Interval ;
y ++ B = A
by Th23;
hence
A is open_interval
by A1, A12; verum