let X be 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 k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL
for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)
let f, g be PartFunc of X,REAL; for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)
let k be positive Real; ( f a.e.= g,M implies a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) )
assume A1:
f a.e.= g,M
; a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)
now for x being object st x in a.e-eq-class_Lp (f,M,k) holds
x in a.e-eq-class_Lp (g,M,k)let x be
object ;
( x in a.e-eq-class_Lp (f,M,k) implies x in a.e-eq-class_Lp (g,M,k) )assume
x in a.e-eq-class_Lp (
f,
M,
k)
;
x in a.e-eq-class_Lp (g,M,k)then consider r being
PartFunc of
X,
REAL such that A2:
(
x = r &
r in Lp_Functions (
M,
k) &
f a.e.= r,
M )
;
r a.e.= f,
M
by A2;
then
r a.e.= g,
M
by A1, LPSPACE1:30;
then
g a.e.= r,
M
;
hence
x in a.e-eq-class_Lp (
g,
M,
k)
by A2;
verum end;
then A3:
a.e-eq-class_Lp (f,M,k) c= a.e-eq-class_Lp (g,M,k)
;
now for x being object st x in a.e-eq-class_Lp (g,M,k) holds
x in a.e-eq-class_Lp (f,M,k)let x be
object ;
( x in a.e-eq-class_Lp (g,M,k) implies x in a.e-eq-class_Lp (f,M,k) )assume
x in a.e-eq-class_Lp (
g,
M,
k)
;
x in a.e-eq-class_Lp (f,M,k)then consider r being
PartFunc of
X,
REAL such that A4:
(
x = r &
r in Lp_Functions (
M,
k) &
g a.e.= r,
M )
;
(
r a.e.= g,
M &
g a.e.= f,
M )
by A1, A4;
then
r a.e.= f,
M
by LPSPACE1:30;
then
f a.e.= r,
M
;
hence
x in a.e-eq-class_Lp (
f,
M,
k)
by A4;
verum end;
then
a.e-eq-class_Lp (g,M,k) c= a.e-eq-class_Lp (f,M,k)
;
hence
a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)
by A3; verum