let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real
for x being Point of (Pre-Lp-Space M,k) st f in x holds
( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real
for x being Point of (Pre-Lp-Space M,k) st f in x holds
( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for k being positive Real
for x being Point of (Pre-Lp-Space M,k) st f in x holds
( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k )
let f be PartFunc of X,REAL ; :: thesis: for k being positive Real
for x being Point of (Pre-Lp-Space M,k) st f in x holds
( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k )
let k be positive Real; :: thesis: for x being Point of (Pre-Lp-Space M,k) st f in x holds
( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k )
let x be Point of (Pre-Lp-Space M,k); :: thesis: ( f in x implies ( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k ) )
assume A1: f in x ; :: thesis: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k )
x in the carrier of (Pre-Lp-Space M,k) ;
then x in CosetSet M,k by VSPDef6X;
then consider h being PartFunc of X,REAL such that
A2: ( x = a.e-eq-class_Lp h,M,k & h in Lp_Functions M,k ) ;
ex g being PartFunc of X,REAL st
( f = g & g in Lp_Functions M,k & h a.e.= g,M ) by A1, A2;
then ex f0 being PartFunc of X,REAL st
( f = f0 & ex ND being Element of S st
( M . (ND ` ) = 0 & dom f0 = ND & f0 is_measurable_on ND & (abs f0) to_power k is_integrable_on M ) ) ;
hence ( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k ) ; :: thesis: verum