Ssreflect 概率事件和非事件总和为 1

问题描述

我是初学者，希望您能帮助将事件 F 的概率与非 F 事件的概率相加为 1。有没有捷径可走？@H_502_1@

X: {RV (P) -> (R)}
F: {set U}
H: 0 < Pr P F
H0: Pr P F < 1
i: U
H1: i \in U

===@H_502_1@

X i * P i * ((if i \in F then R1 else R0) + (if i \in ~: F then R1 else R0)) =
X i * P i

解决方法

在我看来，您需要用 inE 重写，以便 i \in ~: F 变为 i \notin F，然后案例分析 (case: (i \in F)) 后跟 rewrite (addr0,add0r) mulr1 可能够了。