Nuprl Lemma : eo_axioms_wf
∀[r:eo_record{i:l}()]. (eo_axioms(r) ∈ ℙ)
Proof
Definitions occuring in Statement :
eo_axioms: eo_axioms(r),
eo_record: eo_record{i:l}(),
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Lemmas :
subtype_rel_self,
bool_wf,
Id_wf,
nat_wf,
all_wf,
squash_wf,
infix_ap_wf,
less_than_wf,
equal_wf,
not_wf,
isect_wf,
iff_wf,
assert_wf,
eo_record_wf
\mforall{}[r:eo\_record\{i:l\}()]. (eo\_axioms(r) \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-08_33_52
Last ObjectModification:
2015_01_27-PM-02_59_58
Home
Index