Nuprl Lemma : Konig_wf
∀[k:ℕ]. (Konig(k) ∈ ℙ)
Proof
Definitions occuring in Statement :
Konig: Konig(k),
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Lemmas :
all_wf,
nat_wf,
int_seg_wf,
bool_wf,
le_wf,
assert_wf,
subtype_rel_dep_function,
subtype_rel-int_seg,
false_wf,
subtype_rel_self,
not_wf,
exists_wf,
int_seg_subtype-nat
\mforall{}[k:\mBbbN{}]. (Konig(k) \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-08_00_54
Last ObjectModification:
2015_01_27-AM-11_21_59
Home
Index