Nuprl Lemma : not-self-starting_wf
∀[Info,A:Type]. ∀[Y:A ─→ EClass(A)]. (not-self-starting{i:l}(Info;A;Y) ∈ ℙ')
Proof
Definitions occuring in Statement :
not-self-starting: not-self-starting{i:l}(Info;A;Y),
eclass: EClass(A[eo; e]),
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type
Lemmas :
eclass_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
all_wf,
classrel_wf,
not_wf,
eo-forward_wf,
member-eo-forward-E,
es-le-self,
equal_wf,
Id_wf,
es-loc_wf
Latex:
\mforall{}[Info,A:Type]. \mforall{}[Y:A {}\mrightarrow{} EClass(A)]. (not-self-starting\{i:l\}(Info;A;Y) \mmember{} \mBbbP{}')
Date html generated:
2015_07_21-PM-03_12_45
Last ObjectModification:
2015_01_27-PM-07_31_46
Home
Index