let C be non empty set ; for f, h, g being Membership_Func of C holds
( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )
let f, h, g be Membership_Func of C; ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )
A1:
( C = dom (max (f,(min (g,h)))) & C = dom (min ((max (f,g)),(max (f,h)))) )
by FUNCT_2:def 1;
A2:
for x being Element of C st x in C holds
(min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x
proof
let x be
Element of
C;
( x in C implies (min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x )
(min (f,(max (g,h)))) . x =
min (
(f . x),
((max (g,h)) . x))
by Def3
.=
min (
(f . x),
(max ((g . x),(h . x))))
by Def4
.=
max (
(min ((f . x),(g . x))),
(min ((f . x),(h . x))))
by XXREAL_0:38
.=
max (
((min (f,g)) . x),
(min ((f . x),(h . x))))
by Def3
.=
max (
((min (f,g)) . x),
((min (f,h)) . x))
by Def3
.=
(max ((min (f,g)),(min (f,h)))) . x
by Def4
;
hence
(
x in C implies
(min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x )
;
verum
end;
A3:
for x being Element of C st x in C holds
(max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x
proof
let x be
Element of
C;
( x in C implies (max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x )
(max (f,(min (g,h)))) . x =
max (
(f . x),
((min (g,h)) . x))
by Def4
.=
max (
(f . x),
(min ((g . x),(h . x))))
by Def3
.=
min (
(max ((f . x),(g . x))),
(max ((f . x),(h . x))))
by XXREAL_0:39
.=
min (
((max (f,g)) . x),
(max ((f . x),(h . x))))
by Def4
.=
min (
((max (f,g)) . x),
((max (f,h)) . x))
by Def4
.=
(min ((max (f,g)),(max (f,h)))) . x
by Def3
;
hence
(
x in C implies
(max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x )
;
verum
end;
( C = dom (min (f,(max (g,h)))) & C = dom (max ((min (f,g)),(min (f,h)))) )
by FUNCT_2:def 1;
hence
( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )
by A1, A2, A3, PARTFUN1:5; verum