Nuprl Lemma : pv11_p1_upd_bnum_wf
pv11_p1_upd_bnum() ∈ pv11_p1_Ballot_Num() ─→ Id ─→ pv11_p1_Ballot_Num()
Proof
Definitions occuring in Statement :
pv11_p1_upd_bnum: pv11_p1_upd_bnum(),
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
Id: Id,
member: t ∈ T,
function: x:A ─→ B[x]
Lemmas :
pv11_p1_mk_bnum_wf,
subtype_rel_sum,
Id_wf,
pv11_p1_Ballot_Num_wf
Latex:
pv11\_p1\_upd\_bnum() \mmember{} pv11\_p1\_Ballot\_Num() {}\mrightarrow{} Id {}\mrightarrow{} pv11\_p1\_Ballot\_Num()
Date html generated:
2015_07_23-PM-04_10_50
Last ObjectModification:
2015_01_29-AM-11_18_19
Home
Index