let A, B be Element of Family_of_Intervals ; ( A misses B & A \/ B is Interval implies pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) )
assume that
A1:
A misses B
and
A2:
A \/ B is Interval
; pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
A in { I where I is Interval : verum }
by MEASUR10:def 1;
then A3:
ex I being Interval st A = I
;
B in { I where I is Interval : verum }
by MEASUR10:def 1;
then A4:
ex I being Interval st B = I
;
per cases
( A = {} or B = {} or ( A <> {} & B <> {} ) )
;
suppose A7:
(
A <> {} &
B <> {} )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)per cases
( A is closed_interval or A is right_open_interval or A is left_open_interval or A is open_interval )
by A3, MEASURE5:1;
suppose
A is
closed_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A8:
A = [.(inf A),(sup A).]
by A7, MEASURE6:17;
inf A <= sup A
by A7, A8, XXREAL_1:29;
then A9:
(
A is
left_end &
A is
right_end )
by A8, XXREAL_2:33;
per cases
( B is right_open_interval or B is left_open_interval or B is open_interval )
by A4, A10, MEASURE5:1;
suppose
B is
right_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
B = [.(inf B),(sup B).[
by A7, MEASURE6:18;
then A11:
(
inf A = sup B &
A \/ B = [.(inf B),(sup A).] )
by A1, A2, A7, A8, Th15;
then A12:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A7, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A13:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A12, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A13, A9, A11, XXREAL_3:34;
verum end; suppose
B is
left_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
B = ].(inf B),(sup B).]
by A7, MEASURE6:19;
then A14:
(
sup A = inf B &
A \/ B = [.(inf A),(sup B).] )
by A1, A2, A7, A8, Th16;
then A15:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A7, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A16:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A15, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A16, A9, A14, XXREAL_3:34;
verum end; suppose
B is
open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A17:
B = ].(inf B),(sup B).[
by A7, MEASURE6:16;
per cases
( ( inf A = sup B & A \/ B = ].(inf B),(sup A).] ) or ( inf B = sup A & A \/ B = [.(inf A),(sup B).[ ) )
by A1, A2, A7, A8, A17, Th17;
suppose A18:
(
inf A = sup B &
A \/ B = ].(inf B),(sup A).] )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf B <= sup A
by A7, XXREAL_1:26;
then A19:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A18, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A20:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A19, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A20, A9, A18, XXREAL_3:34;
verum end; suppose A21:
(
inf B = sup A &
A \/ B = [.(inf A),(sup B).[ )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf A <= sup B
by A7, XXREAL_1:27;
then A22:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A21, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A23:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A22, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A23, A9, A21, XXREAL_3:34;
verum end; end; end; end; end; suppose
A is
right_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A24:
A = [.(inf A),(sup A).[
by A7, MEASURE6:18;
A25:
A is
left_end
by A7, A24, XXREAL_1:27, XXREAL_2:34;
per cases
( B is closed_interval or B is right_open_interval or B is open_interval )
by A4, A26, MEASURE5:1;
suppose
B is
closed_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A27:
B = [.(inf B),(sup B).]
by A7, MEASURE6:17;
then A28:
(
inf B = sup A &
A \/ B = [.(inf A),(sup B).] )
by A1, A2, A7, A24, Th15;
inf B <= sup B
by A7, A27, XXREAL_1:29;
then A29:
(
B is
left_end &
B is
right_end )
by A27, XXREAL_2:33;
A30:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A28, A7, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A31:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A30, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A31, A29, A28, XXREAL_3:34;
verum end; suppose
B is
right_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A32:
B = [.(inf B),(sup B).[
by A7, MEASURE6:18;
per cases
( ( inf A = sup B & A \/ B = [.(inf B),(sup A).[ ) or ( inf B = sup A & A \/ B = [.(inf A),(sup B).[ ) )
by A1, A2, A7, A24, A32, Th18;
suppose A33:
(
inf A = sup B &
A \/ B = [.(inf B),(sup A).[ )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf B <= sup A
by A7, XXREAL_1:27;
then A34:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A33, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A35:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A34, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A35, A25, A33, XXREAL_3:34;
verum end; suppose A36:
(
inf B = sup A &
A \/ B = [.(inf A),(sup B).[ )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)A37:
B is
left_end
by A7, A32, XXREAL_1:27, XXREAL_2:34;
inf A <= sup B
by A36, A7, XXREAL_1:27;
then A38:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A36, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A39:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A38, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A39, A37, A36, XXREAL_3:34;
verum end; end; end; suppose
B is
open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
B = ].(inf B),(sup B).[
by A7, MEASURE6:16;
then A40:
(
sup B = inf A &
A \/ B = ].(inf B),(sup A).[ )
by A1, A2, A7, A24, Th20;
then
inf B <= sup A
by A7, XXREAL_1:28;
then A41:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A40, A7, MEASURE6:8, MEASURE6:12;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A42:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A41, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A42, A25, A40, XXREAL_3:34;
verum end; end; end; suppose
A is
left_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A43:
A = ].(inf A),(sup A).]
by A7, MEASURE6:19;
A44:
A is
right_end
by A7, A43, XXREAL_1:26, XXREAL_2:35;
per cases
( B is closed_interval or B is left_open_interval or B is open_interval )
by A4, A45, MEASURE5:1;
suppose
B is
closed_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A46:
B = [.(inf B),(sup B).]
by A7, MEASURE6:17;
inf B <= sup B
by A7, A46, XXREAL_1:29;
then A47:
(
B is
left_end &
B is
right_end )
by A46, XXREAL_2:33;
A48:
(
inf A = sup B &
A \/ B = [.(inf B),(sup A).] )
by A1, A2, A7, A43, A46, Th16;
then A49:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A7, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A50:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A49, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A50, A47, A48, XXREAL_3:34;
verum end; suppose
B is
left_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A51:
B = ].(inf B),(sup B).]
by A7, MEASURE6:19;
A52:
B is
right_end
by A7, A51, XXREAL_1:26, XXREAL_2:35;
per cases
( ( inf A = sup B & A \/ B = ].(inf B),(sup A).] ) or ( inf B = sup A & A \/ B = ].(inf A),(sup B).] ) )
by A1, A2, A7, A43, A51, Th21;
suppose A53:
(
inf A = sup B &
A \/ B = ].(inf B),(sup A).] )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf B <= sup A
by A7, XXREAL_1:26;
then A54:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A53, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A55:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A54, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A55, A52, A53, XXREAL_3:34;
verum end; suppose A56:
(
inf B = sup A &
A \/ B = ].(inf A),(sup B).] )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf A <= sup B
by A7, XXREAL_1:26;
then A57:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A56, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A58:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A57, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A58, A44, A56, XXREAL_3:34;
verum end; end; end; suppose
B is
open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A59:
B = ].(inf B),(sup B).[
by A7, MEASURE6:16;
then A60:
(
inf B = sup A &
A \/ B = ].(inf A),(sup B).[ )
by A1, A2, A7, A43, Th22;
then
inf A <= sup B
by A7, XXREAL_1:28;
then A61:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A60, A7, MEASURE6:8, MEASURE6:12;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A62:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A61, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A62, A44, A60, XXREAL_3:34;
verum end; end; end; suppose
A is
open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A63:
A = ].(inf A),(sup A).[
by A7, MEASURE6:16;
per cases
( B is closed_interval or B is left_open_interval or B is right_open_interval )
by A4, A64, MEASURE5:1;
suppose
B is
closed_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A65:
B = [.(inf B),(sup B).]
by A7, MEASURE6:17;
inf B <= sup B
by A7, A65, XXREAL_1:29;
then A66:
(
B is
left_end &
B is
right_end )
by A65, XXREAL_2:33;
per cases
( ( inf A = sup B & A \/ B = [.(inf B),(sup A).[ ) or ( inf B = sup A & A \/ B = ].(inf A),(sup B).] ) )
by A1, A2, A7, A63, A65, Th17;
suppose A67:
(
inf A = sup B &
A \/ B = [.(inf B),(sup A).[ )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf B <= sup A
by A7, XXREAL_1:27;
then A68:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A67, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A69:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A68, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A69, A67, A66, XXREAL_3:34;
verum end; suppose A70:
(
inf B = sup A &
A \/ B = ].(inf A),(sup B).] )
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then
inf A <= sup B
by A7, XXREAL_1:26;
then A71:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A70, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A72:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A71, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A72, A70, A66, XXREAL_3:34;
verum end; end; end; suppose
B is
left_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A73:
B = ].(inf B),(sup B).]
by A7, MEASURE6:19;
A74:
(
sup B = inf A &
A \/ B = ].(inf B),(sup A).[ )
by A1, A2, A7, A63, A73, Th22;
then
inf B <= sup A
by A7, XXREAL_1:28;
then A75:
(
sup (A \/ B) = sup A &
inf (A \/ B) = inf B )
by A74, A7, MEASURE6:8, MEASURE6:12;
A76:
B is
right_end
by A7, A73, XXREAL_1:26, XXREAL_2:35;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A77:
pre-Meas . (A \/ B) = (sup A) - (inf B)
by A7, A75, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A77, A74, A76, XXREAL_3:34;
verum end; suppose
B is
right_open_interval
;
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)then A78:
B = [.(inf B),(sup B).[
by A7, MEASURE6:18;
then A79:
(
sup A = inf B &
A \/ B = ].(inf A),(sup B).[ )
by A1, A2, A7, A63, Th20;
then
inf A <= sup B
by A7, XXREAL_1:28;
then A80:
(
sup (A \/ B) = sup B &
inf (A \/ B) = inf A )
by A79, A7, MEASURE6:8, MEASURE6:12;
A81:
B is
left_end
by A7, A78, XXREAL_1:27, XXREAL_2:34;
pre-Meas . (A \/ B) = diameter (A \/ B)
by A2, Th59;
then A82:
pre-Meas . (A \/ B) = (sup B) - (inf A)
by A7, A80, MEASURE5:def 6;
(
pre-Meas . A = diameter A &
pre-Meas . B = diameter B )
by Th58;
then
(
pre-Meas . A = (sup A) - (inf A) &
pre-Meas . B = (sup B) - (inf B) )
by A7, MEASURE5:def 6;
hence
pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
by A82, A79, A81, XXREAL_3:34;
verum end; end; end; end; end; end;