Nuprl Lemma : pv11_p1_mk_bnum_wf
pv11_p1_mk_bnum() ∈ ℤ ─→ Id ─→ pv11_p1_Ballot_Num()
Proof
Definitions occuring in Statement :
pv11_p1_mk_bnum: pv11_p1_mk_bnum(),
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
Id: Id,
member: t ∈ T,
function: x:A ─→ B[x],
int: ℤ
Lemmas :
subtype_rel_sum,
unit_wf2,
Id_wf
Latex:
pv11\_p1\_mk\_bnum() \mmember{} \mBbbZ{} {}\mrightarrow{} Id {}\mrightarrow{} pv11\_p1\_Ballot\_Num()
Date html generated:
2015_07_23-PM-04_10_47
Last ObjectModification:
2015_01_29-AM-11_18_12
Home
Index