theorem Th61: :: LPSPACE2:61

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for m being positive Real
for r1, r2, r3 being Real st 1 <= m & f in Lp_Functions (M,m) & g in Lp_Functions (M,m) & r1 = Integral (M,((abs f) to_power m)) & r2 = Integral (M,((abs g) to_power m)) & r3 = Integral (M,((abs (f + g)) to_power m)) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))