set f = nilmin_norm ;
FF: for a, b being Element of [.0,1.] holds nilmin_norm . (a,b) = nilmin_norm . (b,a)
proof
let a, b be Element of [.0,1.]; :: thesis: nilmin_norm . (a,b) = nilmin_norm . (b,a)
per cases ( a + b > 1 or a + b <= 1 ) ;
suppose A1: a + b > 1 ; :: thesis: nilmin_norm . (a,b) = nilmin_norm . (b,a)
hence nilmin_norm . (a,b) = min (a,b) by NilminDef
.= nilmin_norm . (b,a) by ;
:: thesis: verum
end;
end;
end;
U1: 1 in [.0,1.] by XXREAL_1:1;
TT: for a being Element of [.0,1.] holds nilmin_norm . (a,1) = a
proof
let a be Element of [.0,1.]; :: thesis: nilmin_norm . (a,1) = a
U4: ( 0 <= a & a <= 1 ) by XXREAL_1:1;
per cases ( a + 1 > 1 or a + 1 <= 1 ) ;
suppose a + 1 > 1 ; :: thesis: nilmin_norm . (a,1) = a
then nilmin_norm . (a,1) = min (a,1) by
.= a by ;
hence nilmin_norm . (a,1) = a ; :: thesis: verum
end;
end;
end;
D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
nilmin_norm . (a,b) <= nilmin_norm . (c,d)
proof
let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies nilmin_norm . (a,b) <= nilmin_norm . (c,d) )
assume S1: ( a <= c & b <= d ) ; :: thesis: nilmin_norm . (a,b) <= nilmin_norm . (c,d)
per cases ( a + b > 1 or a + b <= 1 ) ;
end;
end;
H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds nilmin_norm . (a,0) = 0
proof end;
for a, b, c being Element of [.0,1.] holds nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
proof
let a, b, c be Element of [.0,1.]; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
EE: min (b,c) in [.0,1.] by MinIn01;
U3: min (a,b) in [.0,1.] by MinIn01;
per cases ( ( a + b > 1 & b + c > 1 ) or ( a + b > 1 & b + c <= 1 ) or ( a + b <= 1 & b + c > 1 ) or ( a + b <= 1 & b + c <= 1 ) ) ;
suppose Z1: ( a + b > 1 & b + c > 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then Z2: nilmin_norm . (b,c) = min (b,c) by NilminDef;
per cases ( a + c > 1 or a + c <= 1 ) ;
suppose HU: a + c > 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then W6: a + (min (b,c)) > 1 by ;
W7: c + (min (a,b)) > 1 by ;
nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . (a,(min (b,c))) by
.= min (a,(min (b,c))) by
.= min ((min (a,b)),c) by XXREAL_0:33
.= nilmin_norm . ((min (a,b)),c) by
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum
end;
suppose HU: a + c <= 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
a + (min (b,c)) <= a + c by ;
then W1: a + (min (b,c)) <= 1 by ;
c + (min (a,b)) <= a + c by ;
then W2: c + (min (a,b)) <= 1 by ;
U1: nilmin_norm . (a,b) = min (a,b) by ;
nilmin_norm . (a,(nilmin_norm . (b,c))) = 0 by
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum
end;
end;
end;
suppose Z1: ( a + b > 1 & b + c <= 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then Z2: nilmin_norm . (a,b) = min (a,b) by NilminDef;
per cases ( a + c <= 1 or a + c > 1 ) ;
suppose a + c <= 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then G2: (min (a,b)) + c <= 1 by ;
nilmin_norm . (b,c) = 0 by ;
then nilmin_norm . (a,(nilmin_norm . (b,c))) = 0 by BU
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum
end;
suppose hh: a + c > 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
g4: (min (a,b)) + c = min ((a + c),(b + c)) by FUZZY_2:42
.= b + c by ;
nilmin_norm . (b,c) = 0 by ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) by Z2, g4, BU; :: thesis: verum
end;
end;
end;
suppose Z1: ( a + b <= 1 & b + c > 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then Z2: nilmin_norm . (b,c) = min (b,c) by NilminDef;
ZZ: nilmin_norm . (a,b) = 0 by ;
per cases ( a + c <= 1 or a + c > 1 ) ;
suppose a + c <= 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then G2: (min (b,c)) + a <= 1 by ;
nilmin_norm . ((nilmin_norm . (a,b)),c) = nilmin_norm . (0,c) by
.= nilmin_norm . (c,0) by FF, H1
.= 0 by BU
.= nilmin_norm . (a,(nilmin_norm . (b,c))) by ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum
end;
suppose g5: a + c > 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
g4: (min (c,b)) + a = min ((c + a),(b + a)) by FUZZY_2:42
.= a + b by ;
nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . (a,(min (b,c))) by
.= 0 by
.= nilmin_norm . (c,0) by BU
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by ZZ, FF ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum
end;
end;
end;
suppose Z1: ( a + b <= 1 & b + c <= 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
then Z2: nilmin_norm . (b,c) = 0 by NilminDef;
Z3: nilmin_norm . (a,b) = 0 by ;
nilmin_norm . (a,(nilmin_norm . (b,c))) = 0 by BU, Z2
.= nilmin_norm . (c,0) by BU
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by Z3, FF ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum
end;
end;
end;
hence ( nilmin_norm is commutative & nilmin_norm is associative & nilmin_norm is with-1-identity & nilmin_norm is monotonic ) by ; :: thesis: verum