:: Scaling Properties of Jordan, Borel and Lebesgue Measures under Affine Maps
:: by Noboru Endou and Yasunari Shidama
::
:: Received November 5, 2026
:: Copyright (c) 2026 Association of Mizar Users

Lm1: for b being Real
for X being Subset of REAL holds (AffineMap (0,b)) .: X c= {b}

proof end;

theorem Th1: :: MEASUR16:1

for a, b being Real
for I being Interval holds (AffineMap (a,b)) .: I is Interval

proof end;

Lm2: for a, b, s, t being Real st 0 < a holds
(AffineMap (a,b)) .: [.s,t.] = [.((a * s) + b),((a * t) + b).]

proof end;

Lm3: for a, b, s, t being Real st a < 0 holds
(AffineMap (a,b)) .: [.s,t.] = [.((a * t) + b),((a * s) + b).]

proof end;

Lm4: for a, b, s, t being Real st a = 0 & s <= t holds
(AffineMap (a,b)) .: [.s,t.] = [.b,b.]

proof end;

Lm5: for I being Interval
for a, b being Real st 0 < a & I is closed_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = a * (B-Meas . I)

proof end;

Lm6: for I being Interval
for a, b being Real st a < 0 & I is closed_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = (- a) * (B-Meas . I)

proof end;

Lm7: for I being Interval
for a, b being Real st I is closed_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (B-Meas . I)

proof end;

Lm8: for a, b being Real
for s, t being R_eal st 0 < a holds
(AffineMap (a,b)) .: ].s,t.[ = ].((a * s) + b),((a * t) + b).[

proof end;

Lm9: for I being Interval
for a, b being Real st 0 < a & I is open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = a * (B-Meas . I)

proof end;

Lm10: for a, b being Real
for s, t being R_eal st a < 0 holds
(AffineMap (a,b)) .: ].s,t.[ = ].((a * t) + b),((a * s) + b).[

proof end;

Lm11: for I being Interval
for a, b being Real st a < 0 & I is open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = (- a) * (B-Meas . I)

proof end;

Lm12: for I being Interval
for a, b being Real st I is open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (B-Meas . I)

proof end;

Lm13: for a, b being Real
for s being R_eal
for t being Real st 0 < a holds
(AffineMap (a,b)) .: ].s,t.] = ].((a * s) + b),((a * t) + b).]

proof end;

Lm14: for I being Interval
for a, b being Real st 0 < a & I is left_open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = a * (B-Meas . I)

proof end;

Lm15: for a, b being Real
for s being R_eal
for t being Real st a < 0 holds
(AffineMap (a,b)) .: ].s,t.] = [.((a * t) + b),((a * s) + b).[

proof end;

Lm16: for I being Interval
for a, b being Real st a < 0 & I is left_open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = (- a) * (B-Meas . I)

proof end;

Lm17: for I being Interval
for a, b being Real st I is left_open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (B-Meas . I)

proof end;

Lm18: for a, b, s being Real
for t being R_eal st 0 < a holds
(AffineMap (a,b)) .: [.s,t.[ = [.((a * s) + b),((a * t) + b).[

proof end;

Lm19: for I being Interval
for a, b being Real st 0 < a & I is right_open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = a * (B-Meas . I)

proof end;

Lm20: for a, b, s being Real
for t being R_eal st a < 0 holds
(AffineMap (a,b)) .: [.s,t.[ = ].((a * t) + b),((a * s) + b).]

proof end;

Lm21: for I being Interval
for a, b being Real st a < 0 & I is right_open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = (- a) * (B-Meas . I)

proof end;

Lm22: for I being Interval
for a, b being Real st I is right_open_interval holds
B-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (B-Meas . I)

proof end;

Lm23: for a, b being Real
for I being interval Subset of REAL holds B-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (B-Meas . I)

proof end;

theorem Th2: :: MEASUR16:2

for a, b being Real
for I being interval Subset of REAL holds J-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (J-Meas . I)

proof end;

theorem Th5: :: MEASUR16:3

for X, Y being non empty set
for f being Function of X,Y
for F being Function st rng F c= bool X holds
( dom ((.: f) * F) = dom F & ( for i being object st i in dom ((.: f) * F) holds
((.: f) * F) . i = f .: (F . i) ) )

proof end;

theorem Th4: :: MEASUR16:4

for a, b being Real
for F being FinSequence of Family_of_Intervals holds
( (.: (AffineMap (a,b))) * F is FinSequence of Family_of_Intervals & ( for i being Nat st i in dom ((.: (AffineMap (a,b))) * F) holds
((.: (AffineMap (a,b))) * F) . i = (AffineMap (a,b)) .: (F . i) ) )

proof end;

theorem Th6: :: MEASUR16:5

for X, Y being non empty set
for f being Function of X,Y
for F being FinSequence st rng F c= bool X & f is one-to-one & F is disjoint_valued holds
(.: f) * F is disjoint_valued

proof end;

theorem Th7: :: MEASUR16:6

for X, Y being non empty set
for f being Function of X,Y
for F being Function st rng F c= bool X holds
Union ((.: f) * F) = f .: (Union F)

proof end;

theorem Th8: :: MEASUR16:7

for X being set
for S being non empty Subset-Family of X
for M being Function of S,ExtREAL
for F being FinSequence of S ex x being FinSequence of ExtREAL st
( dom x = dom F & ( for i being Nat st i in dom x holds
x . i = M . (F . i) ) )

proof end;

theorem Th9: :: MEASUR16:8

for X being set
for S being non empty Subset-Family of X
for M being Function of S,ExtREAL
for F being disjoint_valued FinSequence of S
for x being FinSequence of ExtREAL st {} in S & S is cup-closed & M is zeroed & M is additive & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = M . (F . i) ) holds
Sum x = M . (Union F)

proof end;

theorem Th10: :: MEASUR16:9

for r being Real
for x, y being FinSequence of ExtREAL st dom x = dom y & ( for i being Nat st i in dom x holds
y . i = r * (x . i) ) holds
Sum y = r * (Sum x)

proof end;

theorem :: MEASUR16:10

<*{}*> is disjoint_valued FinSequence of Family_of_Intervals

proof end;

theorem Th12: :: MEASUR16:11

for a, b being Real
for I being Element of Field_generated_by Family_of_Intervals holds (AffineMap (a,b)) .: I in Field_generated_by Family_of_Intervals

proof end;

theorem :: MEASUR16:12

for I being Element of Field_generated_by Family_of_Intervals holds
( J-Meas . I = B-Meas . I & J-Meas . I = L-Meas . I )

proof end;

theorem Th14: :: MEASUR16:13

for a, b being Real
for I being Element of Field_generated_by Family_of_Intervals holds J-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (J-Meas . I)

proof end;

theorem Th15: :: MEASUR16:14

for X being set holds .: (id X) = id (bool X)

proof end;

theorem Th16: :: MEASUR16:15

for X, Y being non empty set
for F being Function of X,Y
for S being non empty set st S c= bool X & F is bijective holds
( S is SigmaField of X iff (.: F) .: S is SigmaField of Y )

proof end;

theorem Th17: :: MEASUR16:16

for X, Y being non empty set
for F being Function of X,Y
for S being Subset-Family of X st F is bijective holds
(.: F) .: (sigma S) = sigma ((.: F) .: S)

proof end;

Lm24: for A being Subset of REAL holds Svc (J-Meas,A) = { r where r is R_eal : ex CA being Covering of A, Field_generated_by Family_of_Intervals st r = SUM (vol (J-Meas,CA)) }

proof end;

Field_generated_by Family_of_Intervals c= sigma_Field (C_Meas J-Meas)
by MEASURE8:20;

then Lm25: Borel_Sets c= sigma_Field (C_Meas J-Meas)
by PROB_1:def 9, MEASUR10:6;

theorem Th18: :: MEASUR16:17

for A, B being Subset of ExtREAL
for a being Real st 0 < a & B = { (a * r) where r is R_eal : r in A } holds
( sup B = a * (sup A) & inf B = a * (inf A) )

proof end;

theorem :: MEASUR16:18

for A, B being Subset of ExtREAL
for a being Real st a < 0 & B = { (a * r) where r is R_eal : r in A } holds
( inf B = a * (sup A) & sup B = a * (inf A) )

proof end;

theorem Th20: :: MEASUR16:19

for p, q being sequence of ExtREAL
for a being Real st 0 <= a & ( for n being Element of NAT holds q . n = a * (p . n) ) holds
SUM q = a * (SUM p)

proof end;

theorem Th21: :: MEASUR16:20

for a, b being Real holds (.: (AffineMap (a,b))) .: Family_of_Intervals c= Family_of_Intervals

proof end;

theorem Th22: :: MEASUR16:21

for a, b being Real st a <> 0 holds
(.: (AffineMap (a,b))) .: Family_of_Intervals = Family_of_Intervals

proof end;

theorem Th23: :: MEASUR16:22

for a, b being Real st a <> 0 holds
(.: (AffineMap (a,b))) .: Borel_Sets = Borel_Sets

proof end;

theorem Th24: :: MEASUR16:23

for a, b being Real
for I being Element of Borel_Sets holds (AffineMap (a,b)) .: I in Borel_Sets

proof end;

theorem Th25: :: MEASUR16:24

for a, b being Real
for I being Element of Borel_Sets holds B-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (B-Meas . I)

proof end;

theorem :: MEASUR16:25

for a, b being Real
for I being Element of L-Field holds (AffineMap (a,b)) .: I in L-Field

proof end;

theorem :: MEASUR16:26

for a, b being Real
for I being Element of L-Field holds L-Meas . ((AffineMap (a,b)) .: I) = |.a.| * (L-Meas . I)

proof end;