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 (Lp-Space (M,k)) st f in x holds
( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / 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 (Lp-Space (M,k)) st f in x holds
( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / 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 (Lp-Space (M,k)) st f in x holds
( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) )
let f be PartFunc of X,REAL; :: thesis: for k being positive Real
for x being Point of (Lp-Space (M,k)) st f in x holds
( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) )
let k be positive Real; :: thesis: for x being Point of (Lp-Space (M,k)) st f in x holds
( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) )
let x be Point of (Lp-Space (M,k)); :: thesis: ( f in x implies ( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )
assume A1: f in x ; :: thesis: ( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) )
x in the carrier of (Pre-Lp-Space (M,k)) ;
then x in CosetSet (M,k) by Def11;
then consider g being PartFunc of X,REAL such that
A2: ( x = a.e-eq-class_Lp (g,M,k) & g in Lp_Functions (M,k) ) ;
g in x by A2, Th38;
then ( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) ) by A1, Th50;
hence ( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) by Th53, A1, A2, Th42; :: thesis: verum