let S be non empty finite set ; for D being EqSampleSpaces of S
for s being Element of D
for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
let D be EqSampleSpaces of S; for s being Element of D
for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
let s be Element of D; for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
let f be Function of S,BOOLEAN; Prob (('not' f),s) = 1 - (Prob (f,s))
A1:
s is Element of S *
by FINSEQ_1:def 11;
reconsider s0 = dom s as finite set ;
reconsider CfS = Coim ((f * s),TRUE) as finite set ;
card (Seg (len s)) = len s
by FINSEQ_1:57;
then A2:
card s0 = len s
by FINSEQ_1:def 3;
A3:
Coim ((f * s),TRUE) in bool (dom s)
by A1, Th18;
trueEVENT (('not' f) * s) =
Coim ((('not' f) * s),TRUE)
.=
(dom s) \ (Coim ((f * s),TRUE))
by A1, Th23
;
then A4:
card (trueEVENT (('not' f) * s)) = (card s0) - (card CfS)
by A3, CARD_2:44;
thus Prob (('not' f),s) =
((card s0) / (len s)) - ((card CfS) / (len s))
by A4, XCMPLX_1:120
.=
1 - (Prob (f,s))
by A2, XCMPLX_1:60
; verum