Nuprl Definition : first-member
first-member(T;x;L;P) == ∃i:ℕ||L||. ((x = L[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P L[j]))))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
assert: ↑b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
apply: f a,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
length: ||as||,
equal: s = t ∈ T,
and: P ∧ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
not: ¬A,
assert: ↑b,
apply: f a,
select: L[n]
FDL editor aliases :
first-member
Latex:
first-member(T;x;L;P) == \mexists{}i:\mBbbN{}||L||. ((x = L[i]) \mwedge{} (\muparrow{}(P x)) \mwedge{} (\mforall{}j:\mBbbN{}i. (\mneg{}\muparrow{}(P L[j]))))
Date html generated:
2016_05_15-PM-03_38_12
Last ObjectModification:
2015_09_23-AM-07_44_25
Theory : general
Home
Index