Nuprl Lemma : p-open-member_wf
∀[p:FinProbSpace]. ∀[C:p-open(p)]. ∀[s:ℕ ─→ Outcome]. (s ∈ C ∈ ℙ)
Proof
Definitions occuring in Statement :
p-open-member: s ∈ C,
p-open: p-open(p),
p-outcome: Outcome,
finite-prob-space: FinProbSpace,
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ─→ B[x]
Lemmas :
exists_wf,
nat_wf,
equal-wf-T-base,
subtype_rel_dep_function,
p-outcome_wf,
int_seg_wf,
int_seg_subtype-nat,
false_wf,
subtype_rel_self,
set_wf,
all_wf,
le_wf,
finite-prob-space_wf
\mforall{}[p:FinProbSpace]. \mforall{}[C:p-open(p)]. \mforall{}[s:\mBbbN{} {}\mrightarrow{} Outcome]. (s \mmember{} C \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-07_59_57
Last ObjectModification:
2015_01_27-AM-11_22_12
Home
Index