Nuprl Lemma : pv11_p1_lt_bnum'_wf

[ldrs_uid:Id ─→ ℤ]. (pv11_p1_lt_bnum'(ldrs_uid) ∈ (ℤ × Id) ─→ (ℤ × Id) ─→ 𝔹)


Proof




Definitions occuring in Statement :  pv11_p1_lt_bnum': pv11_p1_lt_bnum'(ldrs_uid) Id: Id bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] product: x:A × B[x] int:
Lemmas :  bor_wf lt_int_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int Id_wf

Latex:
\mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].  (pv11\_p1\_lt\_bnum'(ldrs$_{uid}$)  \mmember{}  (\000C\mBbbZ{}  \mtimes{}  Id)  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Id)  {}\mrightarrow{}  \mBbbB{})



Date html generated: 2015_07_23-PM-04_10_58
Last ObjectModification: 2015_01_29-AM-11_18_13

Home Index