Nuprl Lemma : alist-domain-first
∀[A:Type]
∀d:A List. ∀f1:a:{a:A| (a ∈ d)} ─→ Top. ∀x:A. ∀eq:EqDecider(A).
((x ∈ d)
⇒ (∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))))
Proof
Definitions occuring in Statement :
deq: EqDecider(T),
l_member: (x ∈ l),
select: L[n],
map: map(f;as),
length: ||as||,
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
top: Top,
pi1: fst(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
pair: <a, b>,
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Lemmas :
l_member-first,
all_wf,
int_seg_wf,
not_wf,
equal_wf,
pi1_wf_top,
select_wf,
map_wf,
sq_stable__le,
map-length,
less_than_transitivity2,
le_weakening2,
l_member_wf,
deq_wf,
top_wf,
list_wf,
select-map,
subtype_rel_list,
length_wf,
lelt_wf
\mforall{}[A:Type]
\mforall{}d:A List. \mforall{}f1:a:\{a:A| (a \mmember{} d)\} {}\mrightarrow{} Top. \mforall{}x:A. \mforall{}eq:EqDecider(A).
((x \mmember{} d)
{}\mRightarrow{} (\mexists{}i:\mBbbN{}||d||
((\mforall{}j:\mBbbN{}i. (\mneg{}((fst(map(\mlambda{}x.<x, f1 x>d)[j])) = x))) \mwedge{} ((fst(map(\mlambda{}x.<x, f1 x>d)[i])) = x))))
Date html generated:
2015_07_17-AM-09_16_32
Last ObjectModification:
2015_01_28-AM-07_53_19
Home
Index